Program Chairs
Kousha Etessami
University of Edinburgh
kousha@inf.ed.ac.uk
Sriram Rajamani
Microsoft Research
sriram@microsoft.com
Program Committee
Rajeev Alur, U. Penn
Thomas Ball, Microsoft Research
Alessandro Cimatti, IRST, Trento
Edmund R. Clarke, CMU
E. Allen Emerson, UT Austin
Kousha Etessami, U. Edinburgh
Patrice Godefroid, Bell Labs
Susanne Graf, Verimag
Orna Grumberg, Technion
Nicolas Halbwachs, Verimag
John Hatcliff, Kansas State U.
Thomas A. Henzinger, EPFL
Gerard J. Holzmann, NASA/JPL
Somesh Jha, U. of Wisconsin
Robert B. Jones, Intel Corp.
Orna Kupferman, Hebrew U.
Bob Kurshan, Cadence
Daniel Kroening, CMU
Marta Kwiatowska, U. of Birmingham
Rupak Majumdar, UCLA
Sharad Malik, Princeton U.
Ken McMillan, Cadence
Kedar Namjoshi, Bell Labs
John O'Leary, Intel
Madhusudan Parthasarathy, U. Illinois-Urbana
Doron Peled, U. Warwick
Sriram Rajamani, Microsoft Research
Jakob Rehof, Microsoft Research
Harald Ruess, SRI
Mooly Sagiv, Tel Aviv
Stefan Schwoon, U Stuttgart
Ofer Strichman, Technion
Helmut Veith, TU Munich
Thomas Wilke, Kiel U.
Yaron Wolfsthal, IBM Haifa
Yunshan Zhu, Synopsys
Steering Committee
Edmund M. Clarke, CMU
Mike Gordon, U of Cambridge
Robert P. Kurshan, Cadence
Amir Pnueli, NYU
|
Aims and Scope. CAV'05 conference is the 17th 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. Sample
topics of interest include:
- Algorithms and tools for verifying models and
implementations
- Deductive, compositional, and abstraction techniques for
verification
- Modeling and specification formalisms
- Program analysis and software verification
- Testing and runtime analysis based on verification
technology
- Applications and case studies
- Verification in industrial practice
Invited Speakers:
-
Bob Bentley(Intel),
"Validating a modern microprocessor."
- Bud Mishra (NYU),
""What's Next? Challenges from Systems Biology."
- George Necula (U.C. Berkeley),
"Randomized algorithms for program analysis and verification."
Tutorials:
- Tutorial on Automated abstraction refinement ,
by Thomas Ball (Microsoft) & Ken McMillan (Cadence).
- Tutorial on Theory & practice of decision procedures for combinations
of (first-order) theories,
by Clark Barrett (NYU) and Cesare Tinelli
(U. Iowa).
Satellite Events (July 11-12th):
- BMC'05: 3rd Int. Workshop on Bounded Model Checking.
Organizers: A. Biere & O. Strichman.
- FATES'05:
5th Workshop on Formal Approaches to Testing Software,
Organizers: W. Grieskamp
& C. Weise.
- GDV'05: 2nd Workshop on Games in Design and Verification.
Organizers: M. Jurdzinski & R. Majumdar.
- PDPAR'05: 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning.
Organizers: A. Armando
& A. Cimatti.
-
RV'05:
5th Workshop on Runtime verification,
Organizers:
H. Barringer,
B. Finkbeiner,
Y. Gurevich, &
H. Sipma.
- SoftMC'05: 3rd Workshop on Software Model Checking.
Organizers: B. Cook, S. Stoller, & W. Visser.
- "Satisfiability Modulo Theories Competition", a special tools competition. Organizers: C. Barrett, L. Demoura & A. Stump.
Paper submission. There are two categories of
submissions:
-
-
- A. Regular papers. Submissions
should be in PS or PDF format, should not exceeding thirteen (13)
pages and should use
Springer's LNCS format
with STANDARD margins.
An additional clearly marked appendix may be included
with the submission,
but will only be read
at the discretion of the program committee.
Submissions deviating from these guidelines risk summary rejection.
Submissions 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
strictly forbidden.
- B. Tool presentations. Submissions, not exceeding four (4)
pages
using
Springer's
LNCS format with STANDARD margins, should describe the implemented tool and
its novel features.
An additional clearly marked appendix may be included
with the submission,
but will only be read
at the discretion of the program committee.
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.
The only mechanism for paper submissions is via the electronic
submission web site,
accessible via the
conference homepage.
Important dates.
(EXTENDED & ABSOLUTELY FIRM )
Paper submission deadline:
January 28, 2005
Notification of acceptance/rejection: March 24, 2005
Final version due: April 29, 2005
|