Conference Program
| Sunday, June 28 | Tutorial day | |
|---|---|---|
| 8:15 -- 8:30 |
Invited Tutorial Introductions |
|
| 8:30 -- 09:30 | Tutorial
1, Chair: Amir Pnueli
Joseph Sifakis, (VERIMAG/CNRS, France) Component-based Construction of Heterogeneous Real-time Systems in BIP |
|
| 10:00 -- 10:30 | Break I | |
| 10:30 -- 12:00 | Tutorial
2, Chair: Robert Kurshan Jaeha Kim, (Stanford, US) Mixed-Signal System Verification: A High-Speed Link Example |
|
| 12:00 -- 2:00 | Lunch | |
| 2:00 -- 3:30 | Tutorial
3, Chair: Ahmed Bouajjani Rachid Guerraoui, (EPFL Lausanne, Switzerland) Towards a Theory of Transactional Memory |
|
| 3:30 -- 4:00 | Break II | |
| 4:00 -- 5:30 | Tutorial
4, Chair: Oded Maler Jean Krivine, (Harvard Medical school, US) Analysis and Simulation of Large Molecular Networks in the Kappa Calculus |
|
| Monday, June 29 | Day 1 | |
|---|---|---|
| 8:15 — 8:30 | Welcome | |
| 8:30 — 09:30 | Invited
Talk 1, Chair: Rajeev Alur Ofer Strichman, (Technion, Israel) Regression Verification: Proving the Equivalence of Similar Programs |
|
| 09:30 — 10:00 | Break I | |
| 10:00 — 12:00 | Session 1: Concurrency I, Chair: Roderick Bloem | |
| 10:00 — 10:30 |
Ilan
Beer, Shoham Ben-David, Hana Chockler, Avigail Orni and Richard Trefler |
|
| 10:30 — 11:00 |
Gerard
Basler, Daniel Kroening, Michele Mazzucchi and Thomas Wahl |
|
| 11:00 — 11:30 |
Juan Antonio Navarro
Perez, Andrey Rybalchenko and Atul Singh |
|
| 11:30 — 12:00 | Azadeh Farzan, P.
Madhusudan and Francesco Sorrentino Meta-analysis of Concurrent Program Runs with Nested Locking for Atomicity Violations |
|
| 12:00 — 1:30 | Lunch | |
| 1:30 — 3:30 | Session 2: Concurrency II, Chair: Tayssir Touili | |
| 1:30 — 2:00 |
Peter Lammich, Markus Müller-Olm and Alexander Wenner |
|
| 2:00 — 2:30 |
Salvatore
La Torre, P.
Madhusudan and Gennaro Parlato Reducing Context-bounded Concurrent Reachability to Sequential Reachability |
|
| 2:30 — 3:00 | Shuvendu
Lahiri, Shaz
Qadeer and Zvonimir Rakamaric Static and Precise Detection of Concurrency Errors in Systems Code using SMT solver |
|
| 3:00 — 3:30 | Rachid
Guerraoui, Thomas
Henzinger and Vasu Singh Software Transactional Memory on Relaxed Memory Models |
|
| 3:30 — 4:00 | Break II | |
| 4:00 — 6:00 | Session 3: Applications, Chair: Stravos Tripakis | |
| 4:00 — 4:30 | Nicolas
Coste, Holger
Hermanns, Etienne Lantreibecq and Wendelin Serwe Towards Compositional Performance Prediction of Industrial GALS Designs |
|
| 4:30 — 5:00 | Aditya
Kanade, Rajeev
Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan and
K.C. Shashidhar Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models |
|
| 5:00 — 5:30 | Warren
Hunt and Sol Swords Centaur Technology Media Unit Verification |
|
| 5:30 — 6:00 | Roope
Kaivola, Rajnish
Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra
Pandav, Anna Slobodova, Christopher Taylor, Vladimir Frolov, Erik
Reeber and Armaghan Naik Replacing Testing with Formal Verification in Intel Core i7 Processor Execution Engine Validation |
|
| 6:00 — 10:30 | Reception | |
| Tuesday, June 30 | Day 2 | |
|---|---|---|
| 8:30 — 09:30 | Invited
Talk 2, Chair: Helmut Veith Martin Abadi (UC Santa Cruz and MSR Silicon Valley, US) Models and Proofs of Protocol Security: A Progress Report |
|
| 09:30 — 10:00 | Break I | |
| 10:00 — 12:00 | Session 4: Decision procedures, Chair: Ofer Strichman | |
| 10:00 — 10:30 | Oded
Fuhrmann and Shlomo Hoory On Extending Bounded Proofs to Inductive Proofs |
|
| 10:30 — 11:0 | Jie-Hong Jiang Quantifier Elimination via Functional Composition |
|
| 11:00 — 11:3 | Yeting Ge and Leonardo de
Moura Complete Instantiation for Quantified SMT Formulas |
|
| 11:30 — 12:00 | Swen Jacobs Incremental Instance Generation in Local Reasoning |
|
| 12:00 — 1:00 | Lunch | |
| 1:30 — 3:00 | Session 5: Reduction Techniques, Chair: Markus Müller-Olm | |
| 1:30 — 2:00 | Vineet Kahlon, Chao Wang
and Aarti Gupta An Optimal Symbolic Partial Order Reduction Technique |
|
| 2:00 — 2:30 | Pavol Cerny and Rajeev
Alur Automated Analysis of Java Methods for Confidentiality |
|
| 2:30 — 3:00 | Ru-Gang Xu and Rupak
Majumdar Reducing Test Inputs using Information Partitions |
|
| 2:30 — 3:00 | Break II | |
| 3:00 — 4:30 | Session 6: Numerical Programs and Termination, Chair: Sanjit Seshia | |
| 3:00 — 3:30 | Amir Ben-Amram Size-Change Termination, Monotonicity Constraints and Ranking Functions |
|
| 3:30 — 4:00 | Radu Iosif, Marius Bozga,
Peter Habermehl, Tomas Vojnar and Filip Konecny Automatic Verification of Integer Array Programs |
|
| 4:00 — 4:30 | Sven Verdoolaege, Gerda
Janssens and Maurice Bruynooghe Equivalence Checking of Static Affine Programs using Widening to Handle Recurrences |
|
| 5:00 — 11:00 | Social Event | |
| Wenesday, July 1 | Day 3 | |
|---|---|---|
| 8:30 — 09:30 | Invited
Talk 3, Chair: Klaus havelund Luca Benini (U Bologna; Italy) Predictability vs. Efficiency in the Multicore Era |
|
| 09:30 — 10:00 | Break I | |
| 10:00 — 12:00 | Session 7: Tools I, Chair: Kevin Jones | |
| 10:00 — 10:15 | Michael Ryabtsev and Ofer
Strichman Translation validation: from Simulink to C |
|
| 10:15 — 10:30 |
Alessio Lomuscio, Hongyang
Qu and Franco Raimondi MCMAS: A Model Checker for the verification of Multi-Agent System |
|
| 10:30 — 10:45 | Susmit Jha, Rhishikesh
Limaye and Sanjit A. Seshia Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic |
|
| 10:45 — 11:00 | Saurabh Srivastava, Sumit
Gulwani and Jeffrey Foster VS3: SMT Solvers for Program Verification |
|
| 11:00 — 11:15 | Pallavi Joshi, Mayur Naik,
Chang-Seo Park and Koushik Sen
An Extensible Active Testing Framework for Concurrent Programs |
|
| 11:15 — 11:30 | Sylvain Halle and Roger
Villemaire Browser-based Enforcement of Interface Contracts in Web Applications with BeepBeep |
|
| 11:30 — 11:45 | Ashutosh Gupta and Andrey
Rybalchenko InvGen: An efficiant invariant generator |
|
| 11:45 — 12:00 | Jun Sun, Yang Liu, Jin
Song
Dong and Jun Pang Towards Flexible Verification under Fairness |
|
| 12:00 — 1:30 | Lunch | |
| 1:30 — 3:00 | Session 8: Hybrid Systems, Chair: Martin Fränzle | |
| 1:30 — 2:00 | Colas Le Guernic and
Antoine Girard Reachability Analysis of Hybrid Systems using Support Functions |
|
| 2:00 — 2:30 | Thao Dang and David
Salinas Image Computation for Polynomial Dynamical Dystems using Bernstein Expansion |
|
| 2:30 — 3:00 | Alessandro Cimatti, Marco
Roveri and
Stefano Tonetta Requirements Validation for Hybrid Systems |
|
| 3:00 — 3:30 | Break II | |
| 3:30 — 5:30 | Session 9: Composition and Probability, Chair: Daniel Kröning | |
| 3:30 — 4:00 | Nathan Kitchen and Andreas
Kuehlmann A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints |
|
| 4:00 — 4:30 | Thomas A. Henzinger, Maria
Mateescu and Verena Wolf Sliding Window Abstraction for Infinite Markov Chains |
|
| 4:30 — 5:00 | Ananda Basu, Saddek
Bensalem, Doron Peled and Joseph Sifakis Priority Scheduling of Distributed Systems Based on model Checking |
|
| 5:00 — 5:30 | Shuvendu Lahiri, Shaz
Qadeer, Juan Galeotti, Jan Voung and Thomas Wies Intra-module inference |
|
| 5:30 — 6:30 | Business Meeting | |
| Thursday, July 2 | Day 4 | |
|---|---|---|
| 8:30 — 09:30 | Invited
Talk 4, Chair: Kenneth McMillan Sumit Gulwani (MSR Redmond, US) SPEED: Symbolic Complexity Bound Analysis |
|
| 09:30 — 10:00 | Break I | |
| 10:00 — 12:00 | Session 10: Tools II, Chair: Fabio Somenzi | |
| 10:00 — 10:15 | Saddek Bensalem, Marius
Bozga, Thanh-Hung Nguyen and Joseph Sifakis D-Finder: A Tool for Compositional Deadlock Detection and Verification |
|
| 10:15 — 10:30 |
Christoph Wintersteiger,
Youssef Hamadi and
Leonardo de Moura A Concurrent Portfolio Approach to SMT Solving |
|
| 10:30 — 10:45 | David Hopkins and Luke Ong Homer: a Higher-order Observational equivalence Model checkER |
|
| 10:45— 11:00 | Minxue Pan, Lei Bu and
Xuandong Li TASS: Timing Analyzer of Scenario-Based Specifications |
|
| 11:00 — 11:15 | Khalil Ghorbal, Eric
Goubault and Sylvie Putot The Zonotope Abstract Domain Taylor1+ |
|
| 11:15 — 11:30 | Olivier Bouissou, Eric
Goubault, Sylvie Putot, Karim Tekkal and Franck Vedrin HybridFluctuat: a Static Analyzer of Numerical Programs within a Continuous Environment |
|
| 11:30 — 11:45 | Ernst Moritz Hahn, Holger
Hermanns, Björn Wachter and Lijun Zhang INFAMY: An Infinite-State Markov Model Checker |
|
| 11:45— 12:00 | Bertrand Jeannet and
Antoine
Miné APRON: A Library of Numerical Abstract Domains for Static Analysis |
|
| 12:00 — 1:30 | Lunch | |
| 1:30 — 3:00 | Session 11: Games, Chair: Philippe Schnoebelen | |
| 1:30 — 2:00 | Thomas Gawlitza and Helmut
Seidl Games through Nested Fixpoints |
|
| 2:00 — 2:30 | Roderick Bloem, Krishnendu
Chatterjee, Thomas Henzinger and Barbara Jobstmann Better Quality in Synthesis through Quantitative Objectives |
|
| 2:30 — 3:00 | Emmanuel Filiot, Naiyong
Jin and Jean-François Raskin An Antichain Algorithm for LTL Realizability |
|
| 3:00 — 3:30 | Break II | |
| 3:30 — 5:30 | Session 12: Linear Constraints, Chair: Yassine Lakhnech | |
| 3:30 — 4:00 | Isil Dillig, Thomas Dillig
and Alex Aiken Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers |
|
| 4:00 — 4:30 | David Monniaux On Using Floating-point Computations to Help an Exact Linear Arithmetic Decision Procedure |
|
| 4:30 — 5:00 | Nikolaj Bjorner and Joe
Hendrix Linear Functional Fixed-Points |
|
| 5:00 — 5:30 | Andreas Kuehlmann, Kenneth
McMillan and Shmuel Sagiv Generalizing DPLL to Richer Logics |
|
| 5:30 | End of CAV2009 | |