CAV'01 CALL FOR PAPERS CONFERENCE ON COMPUTER AIDED VERIFICATION July 18-22, 2001 Paris, France URL: http://www.lsv.ens-cachan.fr/cav01 CAV'01 conference is the thirteenth in a series dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. Topics of interest include: * Modeling and specification formalisms (such as logical, automata-based, and algebraic methods) ; * Algorithms and tools (such as state-space exploration, model-checking, synthesis, automated deduction, and proof-checking) ; * Verification techniques (such as state-space and transition-relation reduction methods, symbolic methods, probabilistic methods, compositional and modular reasoning, theorem proving, proof checking, and integration of algorithmic and deductive methods) ; * Applications and case studies (such as synchronous and asynchronous circuits, communication protocols, distributed algorithms, real-time and embedded control systems, security) ; * Testing based on verification technology ; * Verification in practice (integration of verification with design, specification, testing, debugging, and code generation). SUBMISSION INFORMATION The conference will include contributed papers, tool presentations, and invited lectures. There are two categories of submissions: A. Regular papers. Submissions should include an extended abstract not exceeding ten (10) pages. The submission 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. Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed. B. Tool presentations. Submissions should be an abstract not exceeding four (4) pages. The same page limit (4) applies to the conference proceedings. The submission 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 this conference before will be accepted only if significant and clear enhancements to the tool are reported and implemented. Authors are strongly encouraged to use the electronic submission procedure to be provided on the CAV'01 web page http://www.lsv.ens-cachan.fr/cav01 or send a message with subject "submission information" to cav01@lsv.ens-cachan.fr People who do not have access to the net can send ten (10) hard-copies of the submission to A. Finkel Laboratoire Specification et Verification - CNRS UMR 8643 Ecole Normale Superieure de Cachan 61, Avenue du President Wilson 94235 CACHAN CEDEX - FRANCE Each submission should start with a title page containing the category (A or B), the title of the paper, each author's name and affiliation, the contact author's physical and e-mail addresses, phone number, a one- or two-paragraph abstract, and a list of keywords. The submissions must consist of a postcript file, ten pages long, preferably following the LNCS guidelines (see http://www.springer.de/comp/lncs/authors.htm), sent to cav01@lsv.ens-cachan.fr. The submission may include in addition an appendix containing technical details which may be useful in evaluating the merits of the paper and may or may not be read by the reviewers. Please direct all inquiries about CAV'01 to cav01@lsv.ens-cachan.fr IMPORTANT DATES Submission deadline (firm): January 15, 2001 Notification of acceptance: March 21, 2001 Proceedings version of accepted papers due: April 16, 2001 Conference: July 18-22, 2001 Submissions that are not received by 15 January 2001, and submissions that exceed the page limit run the risk of automatic rejection. CHAIRPERSONS Gerard Berry (berry@sophia.inria.fr) INRIA Sophia-Antipolis & EMP Hubert Comon (comon@lsv.ens-cachan.fr, comon@theory.stanford.edu) LSV, ENS Cachan & Stanford University Alain Finkel (finkel@lsv.ens-cachan.fr) LSV, ENS Cachan PROGRAM COMMITTEE Rajeev Alur (U. Penn and Bell Labs) Henrik Reif Andersen (ITU Copenhagen) Gerard Berry, co-chair (INRIA Sophia-Antipolis) Randy Bryant (CMU) Jerry Burch (Cadence) Ching Tsun Chou (Intel) Ed Clarke (CMU) Hubert Comon, co-chair (LSV & Stanford) David Dill (Stanford) E. Allen Emerson, (U. Texas-Austin) Alain Finkel, co-chair (LSV) Patrice Godefroid (Bell Labs) Orna Grumberg (Technion, Israel) Somesh Jha (U. Wisconsin) Bengt Jonsson (Uppsala) Robert Kurshan (Bell Labs) Kim Larsen (Aalborg) Ken McMillan (Cadence) Kedar Namjoshi (Bell Labs) Christine Paulin-Mohring (U. Paris Sud) Carl Pixley (Motorola) Kavita Ravi (Cadence) Natarajan Shankar (SRI) Mary Sheeran (Chalmers & Prover Technology) Tom Shiple (Synopsys) A. Prasad Sistla (U. Illinois-Chicago) Fabio Somenzi (U. Colorado) Yaron Wolfsthal (IBM) CAV STEERING COMMITTEE Edmund Clarke (CMU) Robert Kurshan (Bell Labs) Amir Pnueli (Weizmann) Joseph Sifakis (Verimag)