CAV 2010
22nd International Conference on Computer Aided Verification
Edinburgh, UK, July 15-19, 2010
Program
Program of CAV
Program of CAV
Thursday, July 15th
09:00‑10:00 Tutorial 1
Chair: Paul Jackson
Robert Brayton
ABC: An Academic Industrial-Strength Verification Tool
10:00‑10:30 Break
10:30‑11:00 Tutorial 1 continued
11:00‑12:30 Tutorial 2
Chair: Bob Kurshan
Ken McMillan
Software Model Checking
14:00‑15:00 Tutorial 3
Chair: Tayssir Touili
Thomas Reps
There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code
15:00‑15:30 Break
15:30‑16:00 Tutorial 3 continued
16:00‑17:30 Tutorial 4
Chair: Byron Cook
Andrey Rybalchenko
Constraint Solving for Program Verification: Theory and Practice by Example
Friday, July 16th
09:00‑10:00 FLoC Plenary Talk
Chair: Paul Jackson
09:00 David Basin
Policy Monitoring in First-order Temporal Logic
10:30‑12:30 Software Model Checking
Chair: Orna Grumberg
10:30 Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine and Mihaela Sighireanu
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data
10:55 Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich and Christoph M. Wintersteiger
Termination Analysis with Compositional Transition Invariants
11:20 Kenneth McMillan
Lazy Annotation for Program Testing and Verification
11:45 Thomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar and Jakob Lichtenberg
The Static Driver Verifier Research Platform
12:00 Ming Kawaguchi, Patrick M. Rondon and Ranjit Jhala
Dsolve: Verification Via Liquid Type Inference
12:15 Sudipta Kundu, Malay Ganai and Chao Wang
CONTESSA: Concurrency Testing Augmented with Symbolic Analysis
14:00‑14:50 Model Checking and Automata
Chair: Roderick Bloem
14:00 Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukas Holik, Chih-Duo Hong, Richard Mayr and Tomas Vojnar
Simulation Subsumption in Ramsey-based Buchi Automata Universality and Inclusion Testing
14:25 Frederic Herbreteau, B Srivathsan and Igor Walukiewicz
Efficient Emptiness Check for Timed Buchi Automata
15:30‑16:30 Tools
Chair: David Monniaux
15:30 Nicolas Caniart
Merit: an Interpolating Model-Checker
15:45 Alexandre Donze
Breach, A Simulation-based Toolbox for the Verification and Parameter Synthesis of Hybrid Systems
16:00 Amir Pnueli, Yaniv Sa'ar and Lenore D. Zuck
JTLV : A Framework for Developing Verification Algorithms
16:15 Roland Meyer and Tim Strazny
Petruchio: From Dynamic Networks to Nets
16:30‑18:00 In Memory of Amir Pnueli
Chair: Doron Peled
16:30 Moshe Vardi
Amir Pnueli: Ahead of His Time
17:30 Doron Peled, Zohar Manna and others
Reminiscences on Amir Pnueli
19:00‑23:59 FLoC Reception at National Gallery of Scotland
Saturday, July 17th
09:00‑10:00 Invited Talk
Chair: Helmut Veith
09:00 Pasquale Malacaria
Quantitative Information Flow: from Theory to Practice?
10:30‑12:35 Counter and Hybrid Systems Verification
Chair: Rajeev Alur
10:30 Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci
Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems
10:55 Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns and Ernst Moritz Hahn
Safety Verification for Probabilistic Hybrid Systems
11:20 Khalil Ghorbal, Eric Goubault and Putot Sylvie
A Logical Product Approach to Zonotope Intersection
11:45 Radu Iosif, Marius Bozga and Filip Konecny
Fast Acceleration of Ultimately Periodic Relations
12:10 Luca Pulina and Armando Tacchella
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks
14:00‑14:50 Memory Consistency
Chair: Ganesh Gopalakrishnan
14:00 Jade Alglave, Luc Maranget, Susmit Sarkar and Peter Sewell
Fences in Weak Memory Models
14:25 Sela Mador-Haim, Rajeev Alur and Milo M. K. Martin
Generating Litmus Tests for Contrasting Memory Consistency Models
15:30‑17:10 Verification of Hardware and Low Level Code
Chair: Daniel Kroening
15:30 Aditya Thakur, Junghee Lim, Akash Lal, Amanda Burton, Evan Driscoll, Matt Elder, Tycho Andersen and Thomas Reps
Directed Proof Generation for Machine Code
15:55 Christopher Conway and Clark Barrett
Verifying Low-Level Implementations of High-Level Datatypes
16:20 Satrajit Chatterjee and Michael Kishinevsky
Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics
16:45 Juncao Li, Fei Xie, Thomas Ball and Vladimir Levin
Efficient Reachability Analysis of Buchi Pushdown Systems for Hardware/Software Co-verification
17:15‑17:45 Tools
Chair: Karen Yorav
17:15 Stefan Blom, Jaco van de Pol and Michael Weber
LTSMIN: Distributed and Symbolic Reachability
17:30 Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider and David R. Piegdon
libalf: the Automata Learning Framework
18:00‑19:00 Business Meeting
Sunday, July 18th
09:00‑10:00 Invited Talk
Chair: Vineet Kahlon
09:00 Somesh Jha
Retrofitting Legacy Code for Security
10:00‑10:15 CAV Award Ceremony
10:30‑12:40 Synthesis
Chair: Kedar Namjoshi
10:30 Rudiger Ehlers
Symbolic Bounded Synthesis
10:55 Krishnendu Chatterjee, Thomas Henzinger, Barbara Jobstmann and Rohit Singh
Measuring and Synthesizing Systems in Probabilistic Environments
11:20 Susanne Graf, Doron Peled and Sophie Quinton
Achieving Distributed Control Through Model Checking
11:45 Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas Henzinger and Barbara Jobstmann
Robustness in the Presence of Liveness
12:10 Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Koenighofer, Marco Roveri, Viktor Schuppan and Richard Seeber
RATSY - A new Requirements Analysis Tool with Synthesis
12:25 Viktor Kuncak, Mikael Mayer, Ruzica Piskac and Philippe Suter
Comfusy: A Tool for Complete Functional Synthesis
14:00‑15:00 FLoC Keynote Talk
14:00 Deepak Kapur
Induction, Invariants, and Abstraction.
15:30‑17:35 Concurrent Program Verification I
Chair: Azadeh Farzan
15:30 Vineet Kahlon and Chao Wang
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs
15:55 Viktor Vafeiadis
Automatically proving linearizability
16:20 Pavol Cerny, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri and Rajeev Alur
Model Checking of Linearizability of Concurrent List Implementations
16:45 Ernie Cohen, Michal Moskal, Stephan Tobies and Wolfram Schulte
Local Verification of Global Invariants in Concurrent Programs
17:10 Aws Albarghouthi, Arie Gurfinkel, Ou Wei and Marsha Chechik
Abstract Analysis of Symbolic Executions
17:35‑17:50 Competition Results
17:35 Clark Barrett, Morgan Deters, Albert Oliveras and Aaron Stump
Report on SMT-COMP 2010
19:30‑23:59 FLoC Banquet at Prestonfield House
Monday, July 19th
09:00‑10:00 Invited Talk
Chair: Markus Mueller-Olm
09:00 Maged Michael
Memory Management in Concurrent Algorithms
10:30‑12:00 Compositional Reasoning
Chair: Natasha Sharygina
10:30 Yu-Fang Chen, Edmund Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay and Bow-Yaw Wang
Automated Assume-Guarantee Reasoning through Implicit Learning
10:55 Rishabh Singh, Dimitra Giannakopoulou and Corina Pasareanu
Learning Component Interfaces with May and Must Abstractions
11:20 Ariel Cohen, Kedar Namjoshi and Yaniv Sa'ar
A Dash of Fairness for Compositional Reasoning
11:45 Ariel Cohen, Kedar Namjoshi and Yaniv Sa'ar
SPLIT: A Compositional LTL Verifier
12:00‑12:30 Tool Session
Chair: Holger Hermanns
12:00 Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri and Ralf Wimmer
A Model Checker for AADL
12:15 Manuel Mazo Jr., Anna Davitian and Paulo Tabuada
PESSOA: A tool for embedded controller synthesis.
14:00‑14:50 Decision Procedures
Chair: Alessandro Cimatti
14:00 Min Zhou, Fei He, Bow-Yaw Wang and Ming Gu
On Array Theory of Bounded Elements
14:25 David Monniaux
Quantifier elimination by lazy model enumeration
15:30‑17:10 Concurrent Program Verification II
Chair: Shaz Qadeer
15:30 Pierre Ganty, Rupak Majumdar and Benjamin Monmege
Bounded Underapproximations
15:55 Anil Seth
Global Reachability in Bounded Phase Multi-Stack Pushdown Systems
16:20 Salvatore La Torre, P Madhusudan and Gennaro Parlato
Model-checking parameterized concurrent programs using linear interfaces
16:45 Alexander Kaiser, Daniel Kroening and Thomas Wahl
Dynamic Cutoff Detection in Parameterized Concurrent Programs
17:10‑17:55 Tool Session
Chair: Kevin Jones
17:10 Ernst Moritz Hahn, Holger Hermanns, Bjorn Wachter and Lijun Zhang
PARAM: A Model Checker for Parametric Markov Models
17:25 Krishnendu Chatterjee, Thomas Henzinger, Barbara Jobstmann and Arjun Radhakrishna
GIST: A Solver for Probabilistic Games
17:40 Alessandro Ferrante, Maurizio Memoli, Margherita Napoli, Mimmo Parente and Francesco Sorrentino
A NuSMV Extension for Graded-CTL Model Checking