CAV'05: Conference Program
The CAV'05 conference and all co-located events take place July 6-12th,
2005.
All events take place at Appleton Tower Lecture Theatres, U. of Edinburgh.
The main CAV'05 conference days are July 7-10th.
On July 7-10th, lunches for CAV'05 participants
will be served at Teviot House,
a short walk from Appleton Tower.
The CAV'05 tutorial day is July 6th.
6 affiliated workshops take place July 11-12th, with 3 on each day
(see below).
(No lunches will be served on July 6th nor on July 11-12th.)
Tutorial Day: Wednesday, July 6, 2005.
(Appleton Tower, Lecture Theatre 2.)
(Chair of sessions: Sriram Rajamani)
- 9:00am-10:30am: Automated Abstraction Refinement I.
By Thomas Ball and Ken McMillan.
(Tom Ball's Tutorial Slides.)
- 10:30am-11:00am Coffee Break.
- 11:00am-12:30pm Automated Abstraction Refinement II.
By Thomas Ball and Ken McMillan.
- 12:30pm-2:00pm Lunch
- 2:00pm-3:30pm Theory and Practice of Decision Procedures
for Combinations of Theories, I.
By Clark Barrett and Cesare Tinelli
(Slides for Cesare Tinelli's tutorial.)
- 3:30pm-4:00pm Coffee Break
- 4:00pm-5:30pm Theory and Practice of Decision Procedures
for Combinations of Theories, II.
By Clark Barrett and Cesare Tinelli.
(Clark Barett's Tutorial Slides.)
- 5:30pm - 7:00pm: Welcome Reception.
Day 1 of main conference: Thursday, July 7th.
(Appleton Tower, Lecture Theatre 4.)
- 8:45am Introduction and Welcome.
- 9:00am-10:00am
Invited speaker: George Necula (U. C. Berkeley).
Randomized Algorithms for Program Analysis and Verification.
(Session Chair: Thomas Ball)
- 10:00am-10:30am Coffee Break.
- 10:30am -12:30pm Abstraction & Refinement
(Session Chair: Kedar Namjoshi)
- Predicate Abstraction via Symbolic Decision Procedures.
Authors: Shuvendu Lahiri, Thomas Ball, Byron Cook
- Interpolant-based Transition Relation Approximation.
Authors: Kenneth McMillan, Ranjit Jhala
- Concrete Model Checking with Abstract Matching and Refinement.
Authors: Corina Pasareanu, Radek Pelánek, Willem Visser
- Abstraction for Falsification.
Authors: Thomas Ball, Orna Kupferman, Greta Yorsh
- 12:30pm-2:00pm Lunch.
- 2:00-4:00pm Bounded Model checking
(Session Chair: Ken McMillan)
- Bounded Model Checking of Concurrent Programs.
Authors: Ishai Rabinovitz, Orna Grumberg
- Incremental and Complete Bounded Model Checking for Full PLTL.
Authors: Keijo Heljanko, Tommi Junttila, Timo Latvala
- Abstraction Refinement for Bounded Model Checking.
Authors: Anubhav Gupta, Ofer Strichman
- Symmetry Reduction in SAT-based Model Checking.
Authors: Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip
- 4:00pm-4:30pm Coffee Break.
- 4:30pm-6:00pm Tool session I.
(Session Chair: Daniel Kroening)
- Saturn: A SAT-based Tool for Bug Detection.
Authors: Yichen Xie, Alex Aiken
- JVer: a Java Verifier.
Authors: Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee,
George Necula
- Building Your Own Software Model Checker Using The BOGOR Extensible
Model Checking Framework.
Authors: Matthew Dwyer, John Hatcliff, Matthew Hoosier, Robby
- Wolf - Bug Hunter for Concurrent Software using Formal Methods.
Authors: Sharon Barner, Ziv Glazberg, Ishai Rabinovitz
- Model Checking x86 Executables with CodeSurfer/x86 and WPDS++.
Authors: Gogul Balakrishnan, Thomas Reps, Nick Kidd, Akash Lal, Junghee Lim,
David Melski, Radu Gruian, Suan Yong, Chi-Hua Chen, Tim Teitelbaum
- The ComFoRT Reasoning Framework.
Authors: Sagar Chaki, James Ivers, Natalia Sharygina, Kurt Wallnau.
Day 2 of main conference. Friday, July 8th.
(Appleton Tower, Lecture Theatre 4.)
- 9:00am-10:00am Invited speaker: Bob Bentley (Intel Corp.).
Validating a Modern Microprocessor
(talk slides).
(Session Chair: Bob Kurshan)
- 10:00am-10:30am Coffee Break.
- 10:30am -12:30pm
Verification of hardware, microcode, & Synchronous systems
(Session Chair: John O'Leary)
- Formal Verification of Pentium 4 Components
with Symbolic Simulation
and Inductive Invariants.
Authors: Roope Kaivola
- Formal Verification of Backward Compatibility of Microcode.
Authors: Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim,
Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer,
Moshe Vardi, Lenore Zuck
- Compositional analysis of floating-point linear
numerical filters.
Authors: David Monniaux
- Syntax-Driven Reachable State Space Construction of Synchronous
Reactive Programs.
Authors: Eric Vecchié, Robert de Simone
- 12:30pm-2:00pm Lunch.
- 2:00-4:00pm Games, and Probabilistic Verification
(Session Chair: Ofer Strichman)
- Program Repair as a Game.
Authors: Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem
- Improved Probabilistic Models for 802.11 Protocol Verification.
Authors: Amitabha Roy, K. Gopinath
- Probabilistic Verification for ``Black-Box'' Systems.
Authors: Håkan Younes
- On Statistical Model Checking of Stochastic Systems.
Authors: Koushik Sen, Mahesh Viswanathan, Gul Agha
- 4:00pm-4:30pm Coffee Break.
- 4:30pm-5:45pm Tool session II.
(Session Chair: John Hatcliff)
- The AVISPA Tool for the Automated Validation of Internet Security
Protocols and Applications.
Authors:
Alessandro Armando,
David Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge
Cuellar, Paul Hankes Drielsma, Pierre-Cyrille Heám, Jacopo
Mantovani, Sebastian Moedersheim,
David von Oheimb, Michaël Rusinowitch,
Judson Santiago, Mathieu Turuani, Luca Viganò, Laurent Vigneron
- The Orchids Intrusion Detection Tool.
Authors: Julien Olivain, Jean Goubault-Larrecq
- TVOC: A Translation Validator for Optimizing Compilers.
Authors: Clark Barrett, Yi Fang, Ben Goldberg, Ying Hu, Amir Pnueli, Lenore Zuck
- Cogent: Accurate theorem proving for program verification.
Authors: Byron Cook, Daniel Kroening, Natalia Sharygina
- F-Soft: Software Verification Platform.
Authors: Franjo Ivancic, Zijiang Yang, Malay K. Ganai,
Aarti Gupta, Ilya Shlyakhter, Pranav Ashar
- 7:00-10:00pm CAV'05 Banquet (Dynamic Earth). In honor
of Prof. Ed Clarke's 60th birthday.
Day 3 of main conference. Saturday, July 9th.
(Appleton Tower, Lecture Theatre 4.)
- 9:00am-10:00am Invited speaker: Bud Mishra (N.Y.U.).
What's Next? Challenges from Systems Biology.
(Session Chair: Ed Clarke)
- 10:00am-10:30am Coffee Break.
- 10:30am -12:00pm Decision procedures and applications
(Session Chair: Sharad Malik)
- Yet another Decision Procedure for Equality Logic.
Authors: Orly Meir, Ofer Strichman
- DPLL(T) with Exhaustive Theory Propagation and its Application to
Difference Logic.
Authors: Robert Nieuwenhuis, Albert Oliveras
- Efficient Satisfiability Modulo Theories via Delayed Theory
Combination.
Authors: Marco Bozzano, Roberto Bruttomesso,
Alessandro Cimatti,
Tommi Junttila, Silvio Ranise, Roberto Sebastiani, Peter van Rossum
- 12:00pm-2:00pm Lunch.
- 2:00-4:00pm
Automata and transition systems
(Session Chair: Orna Grumberg)
- Symbolic Systems, Explicit Properties: on Hybrid Approaches for LTL
Symbolic Model Checking.
Authors: Roberto Sebastiani, Stefano Tonetta, Moshe Vardi
- Efficient Monitoring of Omega-Languages.
Authors: Marcelo d'Amorim, Grigore Rosu
- Verification of Tree Updates for Optimization.
Authors: Michael Benedikt, Angela Bonifati, Sergio Flesca, Avinash Vyas
- Expand, Enlarge and Check... Made efficient.
Authors: Gilles Geeraerts, Jean-François Raskin,
Laurent Van Begin
- 4:00pm-4:30pm Coffee Break.
- 4:30pm-6:00pm Tool session III.
(Session Chair: Helmut Veith)
- Results of the Satisfiability Modulo Theories tool Competition.
(co-located with CAV'05)
Organizers: Clark Barrett, Leonardo Demoura, Aaron Stump
- IIV: An Invisible Invariant Verifier.
Authors: Ittai Balaban, Yi Fang, Amir Pnueli, Lenore Zuck
- Action Language Verifier, Extended.
Authors: Tuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan
- Romeo: A Tool for Analyzing Time Petri Nets.
Authors: Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier Roux
- TRANSYT: a tool for the verification of asynchronous concurrent
systems.
Authors: Enric Pastor, Marco A. Peña, Marc Solé
- Ymer: A Statistical Model Checker.
Authors: Håkan Younes
- 6:15pm-7:15pm CAV'05 Business Meeting.
Day 4 of main conference. Sunday, July 10th.
(Appleton Tower, Lecture Theatre 4.)
- 9:00am-10:30am Program Analysis and Verification I
(Session Chair: John Hatcliff)
- Extended Weighted Pushdown Systems.
Authors: Akash Lal, Thomas Reps, Gogul Balakrishnan
- Incremental Algorithms for Inter-procedural Automaton-based Program
Analysis.
Authors: Christopher Conway, Dennis Dams, Stephen A. Edwards, Kedar Namjoshi
- A policy iteration algorithm for computing fixed points in static
analysis of programs.
Authors: Alexandru Costan, Stéphane Gaubert,
Eric Goubault,
Matthieu Martel, Sylvie Putot
- 10:30am -11:00am Coffee Break.
- 11:00am -12:30pm Program Analysis and Verification II
(Session Chair: P. Madhusudan)
- Data Structure Specifications via Local Equality Axioms.
Authors: Scott McPeak, George C. Necula
- Linear Ranking with Reachability.
Authors: Aaron Bradley, Zohar Manna, Henny Sipma
- Reasoning about Threads Communicating via Locks.
Authors: Vineet Kahlon, Franjo Ivancic, Aarti Gupta
- 12:30pm-2:00pm Lunch.
- 2:00pm-3:30pm Applications of Learning
(Session Chair: Rupak Majumdar)
- Abstraction Refinement via Inductive Learning.
Authors: Alexey Loginov, Thomas Reps, Mooly Sagiv
- Automated Assume-Guarantee Reasoning for Simulation Conformance.
Authors: Sagar Chaki, Edmund Clarke, Nishant Sinha, Prasanna Thati
- Symbolic Compositional Verification by Learning Assumptions.
Authors: Rajeev Alur, P. Madhusudan, Wonhong Nam
- END OF MAIN CAV'05 CONFERENCE
Co-located Events (July 6-12):
- "Satisfiability Modulo Theories Competition" (July 6-10):
a special tools competition. (Appleton Tower, 5th floor computer lab.)
Workshop Day 1, Monday, July 11th.
(Appleton Tower Lecture Theatres, 8:45am-6:30pm.)
- BMC'2005: 3rd Int. Workshop on Bounded Model Checking.
(Appleton Tower, Lecture Theatre 1.)
Organizers: Armin Biere and Ofer Strichman.
- FATES'2005: 5th Workshop on Formal Approaches to Testing Software.
(Appleton Tower, Lecture Theatre 2.)
Organizers: W. Grieskamp and C. Weise.
- SoftMC'2005: 3rd Workshop on Software Model Checking.
(Appleton Tower, Lecture Theatre 3.)
Organizers: Byron Cook, Scott Stoller, and Willem Visser.
Workshop Day 2, Tuesday, July 12th.
(Appleton Tower Lecture
Theatres, 8:45am-6:30pm.)
- GDV'2005 (July 12): 2nd Workshop on Games in Design and Verification.
(Appleton Tower, Lecture Theatre 1.)
Organizers: M. Jurdzinski and R. Majumdar.
- PDPAR'2005 (July 12): 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning.
(Appleton Tower, Lecture Theatre 2.)
Organizers: Alessandro Armando and Alessandro Cimatti.
- RV'2005 (July 12): 5th Workshop on Runtime verification.
(Appleton Tower, Lecture Theatre 3.)
Organizers: H. Barringer, B. Finkbeiner, Y. Gurevich,and H. Sipma.