----------------------------------------------------------------------
*** CALL FOR PARTICIPATION ***
[ Please redistribute. Apologies for multiple postings. ]
VMCAI 2010
The Eleventh International Conference on
Verification, Model Checking, and Abstract Interpretation
Madrid, Spain, January 17-19, 2010
(Co-located with POPL 2010)
http://software.imdea.org/events/vmcai10/
Early registration deadline: December 22, 2009
Hotel registration deadline: December 28, 2009
----------------------------------------------------------------------
VMCAI provides a forum for researchers from the communities of
Verification, Model Checking, and Abstract Interpretation,
facilitating interaction, cross-fertilization, and advancement of
hybrid methods. The program of VMCAI'10 will consist of invited
lectures, invited tutorials, and 21 contributed talks. The full
programme is available at the conference web site.
* Invited Talks:
Javier Esparza (Technical University of Munich):
Analysis of Systems with Stochastic Process Creation
Rustan Leino (Microsoft Research):
Verifying Concurrent Programs with Chalice
Reinhard Wilhelm (Saarland University):
Static Timing Analysis for Hard Real-Time Systems
* Invited Tutorials:
Roberto Giacobazzi (University of Verona):
Abstract Interpretation-based Protection
Joost Pieter Katoen (Aachen University):
Advances in Probabilistic Model Checking
Viktor Kuncak (EPFL Lausanne):
Building a Calculus of Data Structures
* Registration:
Further information on registration for VMCAI is available at the
conference web site: http://software.imdea.org/events/vmcai10/
Further information on accommodation is available at the POPL web
site: http://www.cse.psu.edu/popl/10/
* Program:
Sunday, January 17, 2010
9:00-10:00 Invited Talk
* Reinhardt Wilhelm (Saarland University)
Static Timing Analysis for Hard Real-Time Systems
Coffee break
10:30-11:30 Automata and Monitors
* 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
* 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
* 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
* Roberto Giaccobazzi (University of Verona)
Abstract Interpretation-based Protection
Monday, January 18, 2010
9.00-10.00 Invited Talk
* Rustan Leino (Microsoft Research)
Verifying Concurrent Programs with Chalice
Coffee break
10.30-11:30 Logical Methods
* 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
* 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
* 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
* Joost Pieter Katoen (University of Twente)
Advances in Probabilistic Model Checking
Tuesday, January 19, 2010
9.00-10.00 Invited Talk
* Javier Esparza (Technical University of Munich)
Analysis of Systems with Stochastic Process Creation
Coffee break
10.30-11:30 Temporal Logic
* 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
* 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
* Viktor Vafeiadis.
RGSep Action Inference
* Alexander Malkis, Shaz Qadeer and Shuvendu Lahiri.
Abstract Threads
Coffee break
17:00-18.30 Invited Tutorial
* Viktor Kuncak (EPF Lausanne)
Building a Calculus of Data Structures
----------------------------------------------------------------------
|
