VMCAI 2010 - Call for Participation - Early Reg: Dec 22

[vmcai10-announce at clip.dia.fi.upm.es]

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

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