Eleventh International Conference on
Verification, Model Checking, and Abstract Interpretation
January 17-19, 2010
Madrid, Spain
(co-located with POPL 2010)
Preliminary Program
Sunday, January 17, 2010
8:00 Registration opens
9:00-10:00 Welcome and Invited Talk (Chair: Manuel Hermenegildo)- Reinhardt Wilhelm (Saarland University)
Static Timing Analysis for Hard Real-Time Systems
Coffee break
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
Coffee break
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
Lunch break
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
Coffee break
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
Coffee break
10.30-11:30 Logical Methods (Chair: David Schmidt)
- Vijay D'silva, Daniel Kroening, Mitra Purandare and Georg Weissenbacher.
Interpolant Strength - Kuat Yessenov, Ruzica Piskac and Viktor Kuncak.
Collections, Cardinalities, and Relations
Coffee break
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
Lunch break
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
Coffee break
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
Coffee break
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
Coffee break
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
Lunch break
15.30-16.30 Concurrency (Chair: Sophia Drossopoulou)
- Viktor Vafeiadis.
RGSep Action Inference - Alexander Malkis, Shaz Qadeer and Shuvendu Lahiri.
Abstract Threads
Coffee break
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
Sponsors
|
European Association for Programming Languages and Systems |
|
Microsoft Research |
|
Madrid Institute for Advanced
Studies in Software Development Technologies |
|
Association for Computing Machinery |