Program of CAV



It takes place in Salons de la Mutualité, located rue Saint-Victor, in the 5th arrondissement of Paris (France).

Wednesday 18
8:00 - 9:00 Registration desk for the tutorials
9:00 - 10:30 Tutorial 1:
     - Monadic Logics on Strings and Trees (1) - David Basin
11:00 - 12:30 Tutorial 1:
     - Monadic Logics on Strings and Trees (2) - David Basin
12:30 - 14:30 Lunch break
14:30 - 16:00 Tutorial 2:
     - An overview of constraint solving techniques (1) - Pascal Van Hentenryck
16:00 - 16:30 Coffee break
16:30 - 18:00 Tutorial 2:
     - An overview of constraint solving techniques (2) - Pascal Van Hentenryck
18:30 Panel discussion
Thursday 19
8:00 - 9:00 Registration desk for the conference
9:00 - 9:30 Opening the conference
Claire Dupas, director of ENS Cachan
Michel Bidoit, director of LSV
9:30 - 10:30 Invited talk:
     - Software Documentation and the Verification Process - David Parnas (McMaster University)
10:30 - 11:00 Pause
11:00 - 12:30 Session: model-checking and theorem proving
      - Certifying model-checkers - Kedar Namjoshi (Bell Labs, Lucent Technologies)
     - Formalizing a JVML verifier for initialization in a theorem prover - Yves Bertot (INRIA Sophia)
     - Automated Inductive Verification of Parameterized Protocols - Abhik Roychoudhury (University of Singapore), I.V. Ramakrishnan (SUNY Stony Brook)
12:30 - 14:30 Lunch break
14:30 - 16:00 Session: Automata techniques
     - Efficient Model Checking Via Buechi Tableau Automata - Girish Bhat (Cosine Communications), Rance Cleaveland (SUNY Stony Brook) and Alex Groce (Carnegie-Mellon University)
     - Fast LTL to Buchi Automata Translation - Paul Gastin and Denis Oddoux (University Paris 7)
     - A Practical Approach to Coverage in Model Checking Hana Chockler, Orna Kupferman (Hebrew University), Robert Kurshan (Bell Labs) and Moshe Vardi (Rice University)
16:00 - 16:30 Break
16:30 - 18:00 Session: Verification Core Technology
     - A Fast Bisimulation Algorithm - Agostino Dovier (Universty of Verona), Carla Piazza and Alberto Policriti (University of Udine)
     - Symmetry and Reduced Symmetry in Model-checking - A. Prasad Sistla (University of Illinois at Chicago) and Patrice Godefroid (Bell Labs, Lucent Technologies)
     - Transformation-Based Verification Using Generalized Retiming - Andreas Kuehlmann (Cadence Berkeley Labs) and Jason Baumgartner (IBM, Austin)
17:30 Townhall visit
20:00 PC dinner
Friday 20
9:00 - 10:30 Session: BDD and decision procedures
     - Meta-BDDs: a decomposed representation for layered symbolic manipulation of Boolean functions - Gianpiero Cabodi (Politechnico di Torino)
     - CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination - John Moondanos (Logic Validation Technologies, Intel), Carl Seger (Strategic CAD Labs, Intel), Ziyad Hanna and Daher Kaiss (Logic Validation Technologies, Intel)
     - Finite Instantiations in Equivalence Logic with Uninterpreted Functions - Yoav Rodeh and Ofer Shtrichman (Weizmann Institute and IBM Haifa Research Labs)
10:30 - 11:00 Break
11:00 - 12:30 Session: Abstraction and refinement
     - Model Checking with formula-dependent abstract models - Alexander Asteroth, Christel Baier and Ulrich Assmann (University of Bonn)
     - Verifying Network Protocol Implementations by Symbolic Refinement Checking - Rajeev Alur and Bow-Yaw Wang (University of Pennsylvania)
     - Automatic Abstraction for Verification of Timed Circuits and Systems - Hao Zheng, Eric Mercer and Chris Myers (University of Utah)
12:30 - 14:30 Lunch break
14:30 - 16:00 Session: combinations
     - Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM - Marta Kwiatkowska, Gethin Norman (university of Birmingham) and Roberto Segala (University of Bologna)
     - Analysis of Recursive State Machines - R. Alur (Bell Labs and University of Pennsylvania), K. Etessami and M. Yannakakis (Bell Labs)
     - Parameterized Verification with Automatically Computed Inductive Assertions - T. Arons, A. Pnueli, S. Ruah (Weizmann Institute), J. Xu, and L. Zuck (New York University)
16:00 - 16:30 Break
16:30 - 18:00 Tool presentations: rewriting and theorem-proving techniques
     - EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality and Conservative Transformations - Miroslav N. Velev and Randal E. Bryant (Carnegie Mellon University)
     - AGVI -- Automatic Generation, Verification, and Implementation of Security Protocols - Dawn Song, Adrian Perrig and Doantam Phan (University of California at Berkeley)
     - ICS: Integrated Canonizer and Solver - Jean-Christophe Filliatre (University Paris 11), Sam Owre, Harald Ruess and N. Shankar (SRI)
     - mCRL: A Toolset for Analysing Algebraic Specifications - Stefan Blom, Wan Fokkink (CWI), Jan Friso Groote (Eindhoven University of Technology), Izak van Langevelde, Bert Lisser and Jaco van de Pol (CWI)
     - Truth/SLC - A Parallel Verification Platform for Concurrent Systems - Martin Leucker and Thomas Noll (Aachen University of Technology)
     - The SLAM Toolkit - Thomas Ball and Sriram K. Rajamani (Microsoft Research)
18:15 - 18:45 Demos
19:00 Business meeting
20:30 Banquet
Saturday 21
9:00 - 10:00 Invited talk:
     - Java Bytecode Verification: An Overview - Xavier Leroy (INRIA Rocquencourt and Trusted Logic)
10:00 - 10:30 Break
10:30 - 12:30 Session: infinite state systems
     - Iterating transducers - Dennis Dams (Bell Labs, Lucent Technologies), Yassine Lakhnech (VERIMAG) and Martin Steffen (Christian Albrechts University)
     - Attacking Symbolic State Explosion - Giorgio Delzanno (University of Genova), Jean-Francois Raskin and Laurent Van Begin (Brussels Free University)
     - A Unifying Model Checking Approach for Safety Properties of Parameterized Systems - Monika Maidl (University of Edimburgh)
     - A BDD-based Model Checker for Recursive Programs - Javier Esparza and Stefan Schwoon (Technische Universität München)
12:30 - 14:30 Lunch break
14:30 - 15:30 Session: temporal logics and verification
     - Model Checking the World Wide Web - Luca de Alfaro (University of California at Berkeley)
     - Distributed Model Checking for mu-calculus - Orna Grumberg (Technion), Tamir Heyman (Technion and IBM Haifa Research Labs) and Assaf Schuster (Technion)
15:30 - 16:00 Break
16:00 - 17:45 Tool presentations: Model-checking and automata techniques
     - The Temporal Logic Sugar - Ilan Beer, Shoham Ben-David, Cindy Eisner (IBM Haifa Research Labs), Dana Fisman (IBM Haifa Research Labs and Weizmann Institute), Anna Gringauze and Yoav Rodeh (IBM Haifa Research Labs and Weizmann Institute)
     - TReX: A Tool for Reachability Analysis of Complex Systems - Aurore Annichini (VERIMAG), Ahmed Bouajjani and Mihaela Sighireanu (University Paris 7)
     - BOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction - Peer Johannsen (Siemens, Munich)
     - SDLcheck: A Model Checking Tool - Vladimir Levin, Hüsnü Yenigün (Bell Labs, Lucent Technologies)
     - EASN: Integrating ASN.1 and Model Checking - Vivek K. Shanbhag, K. Gopinath (Indian Institute of Science), Markku Turunen, Ari Ahtiainen (Nokia Research Center) and Matti Luukkainen (University of Helsinki)
     - RTDT: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams - Nina Amla, E. Allen Emerson (University of Texas at Austin), Robert P. Kurshan and Kedar Namjoshi (Bell Labs, Lucent Technologies)
     - TAXYS : A Tool for the Development and Verification of Real-Time Embedded Systems - Etienne Closse, Michel Poize, and Jacques Pulou (France Telecom R&D), Joseph Sifakis (VERIMAG), Patrick Venier, Daniel Weil and Sergio Yovine (France Telecom R&D)
18:15 - 19:15 Demos
19:45 Steering Committee meeting
Sunday 22
9:00 - 10:30 Session: microprocessor verification, cache coherence.
     - Microarchitecture Verification by Compositional Model Checking - R. Jhala (University of California at Berkeley) and K. L. McMillan (Cadence Berkeley Labs)
     - Rewriting for Symbolic Execution of State Machine Models - J Strother Moore (University of Texas at Austin)
     - Using Timestamping and History Variables to Verify Sequential Consistency - Tamarah Arons (Weizmann Institute)
11:00 - 12:30 Session: SAT, BDDs and applications.
     - Benefits of Bounded Model Checking at an Industrial Setting - Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella (University og Genova) and Moshe Y. Vardi (Rice University)
     - Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers - Per Bjesse (Chalmers University of Technology), Tim Leonard and Abdel Mokkedem (Compaq)
     - Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2^m) - Sumio Morioka, Yasunao Katayama and Toshiyuki Yamane (IBM Tokyo Research Labs)
12:30 - 14:30 Lunch break
14:30 - 16:00 Session: Timed automata
     - Job-Shop Scheduling using Timed Automata - Yasmina Abdeddaim and Oded Maler (VERIMAG)
     - As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata - Kim Larsen (Aalborg University and University of Twente), Gerd Behrmann (Aalborg University), Ed Brinksma (University of Twente), Ansgar Fehnker (University of Nijmegen), Thomas Hune (Aarhus University), Paul Pettersson (Uppsals University) and Judi Romijn (University of Nijmegen)
     - Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks - Zhe Dang (Washington State University)
16:00 - 16:30 Break
16:30 - 17:00 Demos




Last modified on 14th June 2001 - cav01@lsv.ens-cachan.fr