Eleventh International Conference on
Verification, Model Checking, and Abstract Interpretation
January 17-19, 2010
(co-located with POPL 2010)
Sunday, January 17, 2010
8:00 Registration opens9:00-10:00 Welcome and Invited Talk (Chair: Manuel Hermenegildo)
- Reinhardt Wilhelm (Saarland University)
Static Timing Analysis for Hard Real-Time Systems
10:30-11:30 Automata and Monitors (Chair: Pierre Ganty)
- RoLei Bu, Jianhua Zhao and Xuandong Li.
Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming
- Meera Sridhar and Kevin Hamlen.
Model-Checking In-lined Reference Monitors
12.00-13.30 Abstract interpretation (Chair: Kwangkeun Yi)
- Liqian Chen, Antoine Mine, Ji Wang and Patrick Cousot.
An abstract domain for discovering interval linear equalities
- Valentin Perrelle and Nicolas Halbwachs.
An analysis of permutations in arrays
- Andy King and Harald Sondergaard.
Automatic Abstraction for Congruences
15.30-16.30 Model Checking (Chair: John Gallagher)
- Jori Dubrovin.
Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing
- Benjamin Aminof, Orna Kupferman and Aniello Murano.
Improved Model Checking of Hierarchical Systems
17:00-18.30 Invited Tutorial (Chair: Anindya Banerjee)
- Roberto Giaccobazzi (University of Verona)
Abstract Interpretation-based Protection
Monday, January 18, 2010
9.00-10.00 Invited Talk (Chair: Gilles Barthe)
- Rustan Leino (Microsoft Research)
Verifying Concurrent Programs with Chalice
10.30-11:30 Logical Methods (Chair: David Schmidt)
- Vijay D'silva, Daniel Kroening, Mitra Purandare and Georg Weissenbacher.
- Kuat Yessenov, Ruzica Piskac and Viktor Kuncak.
Collections, Cardinalities, and Relations
12.00-13.30 Program Verification (Chair: Xavier Rival)
- Alexander Summers and Sophia Drossopoulou.
A Considerate Specification of the Composite Pattern
- Thomas Henzinger, Thibaud B. Hottelier, Laura Kovacs and Andrei Voronkov.
Invariant and Type Inference for Matrices
- Yungbum Jung, Soonho Kong, Bow-Yaw Wang and Kwangkeun Yi.
Deriving Invariants in Propositional Logic by Algorithmic Learning, Decision Procedure, and Predicate Abstraction
15.30-16.30 Quantitative Analysis (Chair: Javier Esparza)
- Bjorn Wachter and Lijun Zhang.
Best Probabilistic Transformers
- Rohit Chadha, Axel Legay, Pavithra Prabhakar and Mahesh Viswanathan.
Complexity bounds for the verification of real-time software
17:00-18.30 Invited Tutorial (Chair: David Monniaux)
- Joost Pieter Katoen (University of Twente)
Advances in Probabilistic Model Checking
20.30-23:00 VMCAI 2010 Banquet
Tuesday, January 19, 2010
9.00-10.00 Invited Talk (Chair: Tom Ball)
- Javier Esparza (Technical University of Munich)
Analysis of Systems with Stochastic Process Creation
10.30-11:30 Temporal Logic (Chair: Ahmed Bouajjani)
- Rajeev Alur and Swarat Chaudhuri.
Temporal Reasoning for Procedural Programs
- Cesar Sanchez and Martin Leucker.
Regular Linear Temporal Logic with Past
12.00-13.30 Shape Analysis (Chair: Greta Yorsh)
- Matthew Might.
Shape Analysis of Higher-Order Programs via Abstract Interpretation
- Mark Marron, Rupak Majumdar, Darko Stefanovic and Deepak Kapur.
Shape Analysis with Reference Set Relations
- Jorg Kreiker, Helmut Seidl and Vesal Vojdani.
Shape Analysis of Low-level C with Overlapping Structures
15.30-16.30 Concurrency (Chair: Sophia Drossopoulou)
- Viktor Vafeiadis.
RGSep Action Inference
- Alexander Malkis, Shaz Qadeer and Shuvendu Lahiri.
17:00-18.30 Invited Tutorial (Chair: Andreas Podelski)
- Viktor Kuncak (EPF Lausanne)
Building a Calculus of Data Structures
18:45-19:45 Special VMCAI-POPL joint session in memory of Amir Pnueli
European Association for
Programming Languages and Systems
Madrid Institute for Advanced
in Software Development Technologies
|Association for Computing Machinery|