[isabelle] CAV call for papers


                     CALL FOR PAPERS


                18th International Conference

             August 16-21, 2006, Seattle, Washington



Aims and Scope:


  CAV'06 is the 18th in a series dedicated to the advancement of the

  theory and practice of computer-assisted formal analysis methods for

  hardware and software systems.  This year, CAV is part of the 4th

  International Federated Logic Conference (FLoC 2006), which includes

  CAV and five other conferences/symposia: ICLP, IJCAR, LICS, RTA, and

  SAT.  More details about FLoC 2006 can be found at



  CAV 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:


  - Algorithms and tools for verifying models and implementations

  - Hardware verification techniques

  - Program analysis and software verification

  - Modeling and specification formalisms

  - Deductive, compositional, and abstraction techniques for


  - Testing and runtime analysis based on verification technology

  - Applications and case studies

  - Verification in industrial practice




  Special Symposium:


    The first day of CAV is traditionally a tutorial day.  This year,

    the tutorial will be replaced with a special symposium entitled

    "25 Years of Model Checking".  The symposium will consist of

    invited lectures delivered by leading researchers in the field of

    model checking.  Topics will include historical perspectives,

    state-of-the-art research, and directions for future research.


  In addition to the special symposium, there will be seven affiliated



    - BMC'06: 4th International Workshop on Bounded Model Checking


    - TV'06: Multithreading in Hardware and Software: Formal

      Approaches to Design and Verification


    - SMT-COMP'06: 2nd Satisfiability Modulo Theories tools competition


    - ACL2'06: 6th International Workshop on the ACL2 Theorem Prover

      and its Applications


    - GDV'06: 3rd International Workshop on Games in Design and



    - V&D'06: 1st International Workshop on Verification on Debugging


    - Verified Software: Tools, Techniques, and Experiments


Paper submission:


  There are two categories of submissions:


    A. Regular papers. Submissions, not exceeding thirteen (13) pages

       using Springer's LNCS format, 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, not exceeding four (4) pages

       using Springer's LNCS format, 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.


  Information concerning the procedure for submissions will be available

  on the conference home page:




  Important dates:


    Paper submission (firm): January 27, 2006

    Notification of acceptance/rejection: April 10, 2006

    Final version due: May 6, 2006


Program Chairs:


  Thomas Ball, Microsoft, tball at microsoft.com

  Robert Jones, Intel, rjones at ichips.intel.com


Program Committee:


  Thomas Ball, Microsoft

  Clark Barrett, NYU

  Karthik Bhargavan, Microsoft

  Per Bjesse, Synopsys

  Ahmed Bouajjani, Univ. Paris 7

  Randy Bryant, CMU

  Rance Cleaveland, Univ. Maryland

  Werner Damm, Univ. Oldenberg

  Ganesh Gopalakrishnan, Univ. Utah

  Steve German, IBM Research

  Patrice Godefroid, Bell Labs

  Mike Gordon, Univ. Cambridge

  Orna Grumberg, Technion

  Holger Hermanns, Saarland Univ.

  Ranjit Jhala, UC San Diego

  Robert Jones, Intel

  Roope Kaivola, Intel

  Ken McMillan, Cadence

  Tom Melham, Oxford Univ.

  Corina Pasareanu, NASA Ames

  Amir Pnueli, NYU

  Thomas Reps, Univ. Wisconsin

  Sanjit Seshia, UC Berkeley

  Prasad Sistla, Univ. Illinois - Chicago

  Fabio Somenzi, Univ. Colorado


Steering Committee:


  Edmund M. Clarke, CMU

  Mike Gordon, U of Cambridge

  Robert P. Kurshan, Cadence

  Amir Pnueli, NYU




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.