[Hol-info] ITP 2012: Final Call for Papers
Final Call for Papers ITP 2012: 3rd International Conference on Interactive Theorem Proving 13-16 August 2012, Princeton, New Jersey, USA http://itp2012.cs.princeton.edu/ ITP is the premier international conference for researchers from all areas of interactive theorem proving and its applications. The inaugural meeting of ITP was held in July 2010 in Edinburgh, Scotland, as part of the Federated Logic Conference (FLoC), and the second meeting took place in Nijmegen, The Netherlands, in August 2011. ITP 2012 will take place in Princeton, New Jersey, USA on 13-16 August 2012 with two workshops preceding the main conference: The Isabelle Workshop 2012 (organized by Tobias Nipkow, Larry Paulson, and Makarius Wenzel) and the 4th Coq Workshop (organized by Adam Chlipala). ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The program committee welcomes submissions on all aspects of interactive theorem proving and its applications. Examples of typical topics include formal aspects of hardware or software (specification, verification, semantics, synthesis, refinement, compilation, etc.); formalization of significant bodies of mathematics; advances in theorem prover technology (automation, decision procedures, induction, combinations of systems and tools, etc.); industrial applications of theorem proving; other topics including those relating to user interfaces, education, comparisons of systems, and mechanizable logics; and concise and elegant worked examples (Proof Pearls). Submission details: All papers must be submitted electronically, via EasyChair: https://www.easychair.org/conferences/?conf=itp2012 Papers may be no longer than 16 pages and are to be submitted in PDF using the Springer LNCS format. Instructions and style files may be found by going to http://www.springer.com/computer/lncs/lncs+authors and downloading the files llncs2e.zip and typeinst.zip. Submissions must describe original unpublished work not submitted for publication elsewhere, presented in a way that users of other systems can understand. The proceedings will be published as a volume in the Springer Lecture Notes in Computer Science series and will be available to participants at the conference. In addition to regular submissions, described above, there will be a rough diamonds section. Rough diamond submissions are limited to six pages and may consist of an extended abstract. They will be refereed and are expected to present innovative and promising ideas, possibly in an early form and without supporting evidence. Accepted diamonds will be published in the main proceedings, and will be presented as short talks. Both regular and rough diamond submissions require an abstract of 70 to 150 words to be submitted electronically at the above address one week before the full submission. All submissions must be written in English. Submissions are expected to be accompanied by verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used. The submission page contains a corresponding file upload function. Authors who have strong reasons (e.g. of commercial/legal nature) for violating this policy should contact the PC chairs in advance. At the time of abstract submission, proof assistants and other tools necessary for evaluating the submission should be indicated using the Keywords section of the web interface. Authors of accepted papers are expected to present their papers at the conference, and will be required to sign copyright release forms. Important dates: Abstract submission deadline: 6 February 2012 Paper submission deadline: 13 February 2012 Notification of paper decisions:13 April 2012 Final versions due from authors:5 May 2012 Pre-conference workshops: 12 August 2012 Conference dates: 13-16 August 2012 Web page: http://itp2012.cs.princeton.edu/ Invited Speakers: Gilles Barthe (IMDEA, Spain) Lawrence Paulson (Univ. of Cambridge, UK) Andre Platzer (Carnegie Mellon Univ., USA) Invited Tutorial: Andrew Gacek (Rockwell Collins, USA) General Co-Chairs: Andrew Appel (Princeton Univ., USA) Lennart Beringer (Princeton Univ., USA) Program Co-Chairs: Lennart Beringer (Princeton Univ., USA) Amy Felty (Univ. of Ottawa, Canada) Program Committee: Andreas Abel (LMU Munich, Germany) Nick Benton (Microsoft Research Cambridge, UK) Stefan Berghofer (secunet Security Networks AG, Germany) Lennart Beringer (Co-Chair, Princeton Univ., USA) Yves Bertot (INRIA Sophia-Antipolis, France) Adam Chlipala (MIT, USA) Ewen Denney (NASA, USA) Peter Dybjer (Chalmers Univ. of Technology, Sweden) Amy Felty (Co-Chair, Univ. of Ottawa, Canada) Herman Geuvers (Radboud Univ. Nijmegen, The Netherlands) Georges Gonthier (Microsoft Research Cambridge,
[Hol-info] COMETS 2012 - 3rd IEEE Track on Collaborative Modeling and Simulation - Call for Papers
(Please accept our apologies if you receive multiple copies of this message) # IEEE WETICE 2012 3rd IEEE Track on Collaborative Modeling and Simulation (Comets 2012) in cooperation with AFIS (INCOSE France Chapter) MIMOS (Italian Association for MS) CALL FOR PAPERS # June 25-27, 2012, Toulouse (France) http://www.sel.uniroma2.it/comets12 # # Papers Due: March 16, 2012 # Accepted papers will be published in the conference proceedings # by the IEEE Computer Society Press and indexed by EI. # Modeling and Simulation (MS) is increasingly becoming a central activity in the design of new systems and in the analysis of existing systems because it enables designers and researchers to investigate systems behavior through virtual representations. For this reason, MS is gaining a primary role in many industrial and research fields, such as space, critical infrastructures, manufacturing, emergency management, biomedical systems and sustainable future. However, as the complexity of the investigated systems increases and the types of investigations widens, the cost of MS activities increases for the more complex models and for the communications among a wider number and variety of MS stakeholders (e.g., sub-domain experts, simulator users, simulator engineers, and final system users). To address the increasing costs of MS activities, collaborative technologies must be introduced to support these activities by fostering the sharing and reuse of models, by facilitating the communications among MS stakeholders, and more generally by integrating processes, tools and platforms. Aside from seeking applications of collaborative technologies to MS activities, the track seeks innovative contributions that deal with the application of MS practices to the design of collaborative environments. These environments are continuously becoming more complex, and therefore their design requires systematic approaches to meet the required quality of collaboration. This is important for two reasons: to reduce rework activities on the actual collaborative environment, and to maximize the productivity and the quality of the process the collaborative environment supports. MS offers the methodologies and tools for such investigations and therefore it can be used to improve the quality of collaborative environments. A non–exhaustive list of topics of interest includes: * collaborative environments for MS * collaborative Systems of Systems MS * workflow modelling for collaborative environments and processes * agent-based MS * collaborative distributed simulation * collaborative component-based MS * net-centric MS * web-based MS * model sharing and reuse * model building and evaluation * modeling and simulation of business processes * modeling for collaboration * simulation-based performance evaluation of collaborative networks * model-driven simulation engineering * domain specific languages for the simulation of collaborative environments * domain specific languages for collaborative MS * databases and repositories for MS * distributed virtual environments * virtual research environment for MS * collaborative DEVS MS To stimulate creativity, however, the track maintains a wider scope and invites interested researchers to present contributions that offer original perspectives on collaboration and MS. +++ On-Line Submissions and Publication +++ CoMetS'12 intends to bring together researchers and practitioners to discuss key issues, approaches, open problems, innovative applications and trends in the track research area. This year, we will accept submissions in two forms: (1) papers (2) poster and industrial presentations (1) Papers should contain original contributions not published or submitted elsewhere. Papers up to six pages (including figures, tables and references) can be submitted. Papers should follow the IEEE format, which is single spaced, two columns, 10 pt Times/Roman font. All submissions should be electronic (in PDF) and will be peer-reviewed by at least three program committee members. Accepted full papers will be included in the proceedings and published by the IEEE Computer Society Press (IEEE approval pending). Please note that at least one author for each accepted paper should register to attend WETICE 2012 (http://www.wetice.org) to have the paper published in the proceedings. (2) Posters should describe a practical, on-the-field, experience in any domain area using collaborative MS. The poster submission requires the submission of an abstract for evaluation from the
[Hol-info] SAT 2012: Call for Papers
[ We apologize if you receive multiple copies of this CFP. ] - 15th International Conference on THEORY AND APPLICATIONS OF SATISFIABILITY TESTING --- SAT 2012 --- Trento, Italy, June 17-20th, 2012 http://sat2012.fbk.eu/ - AIM and SCOPE = The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the primary annual meeting for researchers studying the propositional satisfiability problem. Importantly, here SAT is interpreted in a rather broad sense: besides plain propositional satisfiability, it includes the domains of MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulae (QBF), Satisfiability Modulo Theories (SMT), Constraints Programming (CSP) techniques for word-level problems and their propositional encoding. To this extent, many hard combinatorial problems can be encoded as SAT instances, in the broad sense mentioned above, including problems that arise in hardware and software verification, AI planning and scheduling, OR resource allocation, etc. The theoretical and practical advances in SAT research over the past twenty years have contributed to making SAT technology an indispensable tool in these domains. SAT 2012 will take place in Trento, Italy, a cosmopolitan city set in a spectacular mountain scenery, and home to a world-class university and research centres. RELEVANT TOPICS === The topics of the conference span practical and theoretical research on SAT (in the broader sense above) and its applications, and include, but are not limited to: * Theoretical issues - Combinatorial Theory of SAT - Proof Systems and Proof Complexity in SAT - Analysis of SAT Algorithms * Solving: - Improvements of current solving procedures - Novel solving procedures, techniques and heuristics - Incremental solving * Beyond solving: - Functionalities (e.g., proofs, unsat-cores, interpolants,...) - Optimization * Applications - SAT techniques for other domains - Novel Problem Encodings - Novel Industrial Applications of SAT A more detailed description can be found on the web site. INVITED SPEAKERS We are honored to announce the following invited speakers at SAT 2012: * Aaron Bradley, Boulder, USA. SAT-based Verification with IC3: Foundations and Demands * Donald Knuth, Stanford, USA. Satisfiability and The Art of Computer Programming The presence of both speakers has been confirmed, although the titles of the talks may be provisional. AFFILIATED EVENTS = SAT 2012 is co-located with the 2nd International SAT/SMT Summer School (June 12-15), http://satsmtschool2012.fbk.eu/. SAT 2012 will also host related events like workshops (June 16) and various competitive events. PAPER SUBMISSION Papers must be edited in LATEX using the LNCS format and be submitted electronically as PDF files via EasyChair. We envisage three categories of submissions: REGULAR PAPERS. Submissions, not exceeding fourteen (14) pages, should contain original research, and sufficient detail to assess the merits and relevance of the contribution. For papers reporting experimental results, authors are strongly encouraged to make their data available with their submission. Submissions reporting on case studies in an industrial context are strongly invited, and should describe details, weaknesses and strength in sufficient depth. Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed. TOOL PRESENTATIONS. Submissions, not exceeding six (6) pages, should describe the implemented tool and its novel features. A demonstration is expected to accompany a tool presentation. Papers describing tools that have already been presented in other conferences before will be accepted only if significant and clear enhancements to the tool are reported and implemented. EXTENDED ABSTRACTS/POSTERS. Submissions, not exceeding two (2) pages, briefly introducing work in progress, student work, or preliminary results. These papers are expected to be presented as posters at the conference. Further information about paper submission, including a more detailed description of the scope and specification of the three submission categories, will be made available at SAT 2012 web page. The review process will be subject to a rebuttal phase. IMPORTANT DATES: Abstract Submission: 05/02/2012 Paper Submission: 12/02/2012 Rebuttal phase:28-30/03/2012 Final Notification: 12/04/2012 Final Version Due:04/05/2012 SAT/SMT School:
