Thursday, July 15th
Thursday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Tutorial 1
Chair: Paul Jackson
Location: AT LT4
| 09:00 | Robert Brayton ABC: An Academic Industrial-Strength Verification Tool |
10:30‑11:00 Tutorial 1 continued
Location: AT LT4
11:00‑12:30 Tutorial 2
Chair: Bob Kurshan
Location: AT LT4
| 11:00 | Ken McMillan Software Model Checking (TBC) |
14:00‑15:00 Tutorial 3
Chair: Tayssir Touili
Location: AT LT4
| 14:00 | Thomas Reps There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code |
15:30‑16:00 Tutorial 3 continued
Location: AT LT4
16:00‑17:30 Tutorial 4
Chair: Byron Cook
Location: AT LT4
| 16:00 | Andrey Rybalchenko Constraint Solving for Program Verification: Theory and Practice by Example |
Friday, July 16th
Friday's program is also available with abstracts and side by side with other events.
09:00‑10:00 FLoC Plenary Talk: David Basin
Location: George Square Lecture Theatre
| 09:00 | David Basin (ETH Zurich) Policy Monitoring in First-order Temporal Logic |
10:30‑12:30 Software Model Checking
Chair: Orna Grumberg
Location: AT LT4
| 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
Location: AT LT4
| 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 Büchi Automata Universality and Inclusion Testing |
| 14:25 | Frédéric Herbreteau, B Srivathsan and Igor Walukiewicz Efficient Emptiness Check for Timed Büchi Automata |
15:30‑16:30 Tools
Chair: David Monniaux
Location: AT LT4
| 15:30 | Nicolas Caniart Merit: an Interpolating Model-Checker |
| 15:45 | Alexandre Donzé 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
Location: AT LT4
| 16:30 | Moshe Vardi Amir Pnueli: Ahead of His Time |
| 17:30 | Doron Peled, Zohar Manna and others Reminiscences on Amir Pnueli (TBC) |
Saturday, July 17th
Saturday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Invited Talk
Chair: Helmut Veith
Location: AT LT4
| 09:00 | Pasquale Malacaria Quantitative Information Flow: from Theory to Practice? |
10:30‑12:30 Counter and Hybrid Systems Verification
Chair: Rajeev Alur
Location: AT LT4
| 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
Location: AT LT4
| 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
Location: AT LT4
| 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 Büchi Pushdown Systems for Hardware/Software Co-verification |
17:15‑17:45 Tools
Chair: Karen Yorav
Location: AT LT4
| 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
Location: AT LT4
Sunday, July 18th
Sunday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Invited Talk
Chair: Vineet Kahlon
Location: AT LT4
| 09:00 | Somesh Jha Retrofitting Legacy Code for Security |
10:00‑10:15 CAV Award Ceremony
Location: AT LT4
10:30‑12:30 Synthesis
Chair: Kedar Namjoshi
Location: AT LT4
| 10:30 | Rüdiger 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: Deepak Kapur
Location: George Square Lecture Theatre
| 14:00 | Deepak Kapur (University of New Mexico) Induction, Invariants, and Abstraction |
15:30‑17:35 Concurrent Program Verification I
Chair: Azadeh Farzan
Location: AT LT4
| 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, Michał 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
Location: AT LT4
| 17:35 | Clark Barrett, Morgan Deters, Albert Oliveras and Aaron Stump Report on SMT-COMP 2010 |
Monday, July 19th
Monday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Invited Talk
Chair: Markus Mueller-Olm
Location: AT LT4
| 09:00 | Maged Michael Memory Management in Concurrent Algorithms |
10:30‑12:00 Compositional Reasoning
Chair: Natasha Sharygina
Location: AT LT4
| 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
Location: AT LT4
| 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
Location: AT LT4
| 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
Location: AT LT4
| 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
Location: AT LT4
| 17:10 | Ernst Moritz Hahn, Holger Hermanns, Björn 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 |