2009-12-14

[Caml-list] VMCAI 2010 - Call for Participation - Early Reg: Dec 22

----------------------------------------------------------------------
*** 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

----------------------------------------------------------------------

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

No comments: