Program / Abstracts

Monday, January 17, 2005

8:15 - 9:00 Coffee & Registration
9:00 - 9:30 Welcome
9:30 - 10:30 Invited Speaker (Session Chair: Amir Pnueli)
  • Patrick Cousot (École Normale Supérieure, F)
    Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming
10:30 - 11:00 Coffee
11:00 - 12:30 Numerical Abstraction (Session Chair: Helmut Seidl)
  • Scalable Analysis of Linear Systems using Mathematical Programming

    Sriram Sankaranarayanan (Stanford University)
    Henny Sipma (Stanford University)
    Zohar Manna (Stanford University)

  • The Arithmetic-Geometric Progression Abstract Domain

    Jérôme Feret (École Normale Supérieure)

  • An overview of semantics for the validation of numerical programs

    Matthieu Martel (CEA, Saclay)

12:30 - 14:00 Lunch
14:00 - 15:00 Invited Speaker (Session Chair: Radhia Cousot)
  • C.A.R. Hoare (Microsoft Research, Cambridge, UK)
    The Verifying Compiler, a Grand Challenge for Computing Research
15:00 - 15:30 Coffee
15:30 - 17:30 Verification I (Session Chair: Roberto Giacobazzi)
  • Checking Herbrand Equalities and Beyond

    Markus Müller-Olm (FernUniversität Hagen)
    Oliver Rüthing (Universität Dortmund)
    Helmut Seidl (Technische Universität München)

  • Static analysis by abstract interpretation of the quasi-synchonous composition of synchronous programs

    Julien Bertrane (École Normale Supérieure)

  • Termination of Polynomial Programs

    Aaron Bradley (Stanford University)
    Zohar Manna (Stanford University)
    Henny Sipma (Stanford University)

  • Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement

    Sebastian Burckhardt (University of Pennsylvania)
    Rajeev Alur (University of Pennsylvania)
    Milo Martin (University of Pennsylvania)

Tuesday, January 18, 2005

8:30 - 9:00 Coffee
9:00 - 10:00 Invited Speaker (Session Chair: Agostino Cortesi)
  • Amir Pnueli (New York University, USA & Weizmann Institute of Science, IL)
    Abstraction for Liveness
10:00 - 10:30 Coffee
10:30 - 12:30 Heap & Shape Analysis (Session Chair: David Schmidt)
  • Abstract Interpretation with Alien Expressions and Heap Structures

    Bor-Yuh Evan Chang (University of California, Berkeley)
    K. Rustan M. Leino (Microsoft Research)

  • Shape Analysis by Predicate Abstraction

    Ittai Balaban (New York University)
    Amir Pnueli (New York University, USA & Weizmann Institute of Science, IL)
    Lenore Zuck (University of Illinois at Chicago)

  • Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists

    Roman Manevich (Tel Aviv University)
    Eran Yahav (IBM T.J. Watson)
    Ganesan Ramalingam (IBM T.J. Watson)
    Mooly Sagiv (Tel Aviv University)

  • Purity Analysis for Java Programs

    Alexandru Salcianu (MIT)
    Martin Rinard (MIT)

12:30 - 14:00 Lunch
14:00 - 15:30 Abstract Model Checking (Session Chair: Rustan Leino)
  • Automata As Abstractions

    Dennis Dams (Bell Laboratories)
    Kedar Namjoshi (Bell Laboratories)

  • Don't know in the mu-calculus

    Orna Grumberg (The Technion)
    Martin Lange (LMU Munich)
    Martin Leucker (TU Munich)
    Sharon Shoham (The Technion)

  • Model Checking of Systems Employing Commutative Functions

    A. Prasad Sistla (University of Illinois at Chicago)
    Min Zhou (University of Illinois at Chicago)
    Xiaodong Wang (University of Illinois at Chicago)

15:30 - 16:00 Coffee
16:00 - 18:00 Model Checking (Session Chair: Sriram Rajamani)
  • Weak automata for the linear time mu-calculus

    Martin Lange (University of Munich)

  • Model checking for Process Rewrite Systems and a class of action-based regular properties

    Laura Bozzelli (Università di Napoli)

  • I/O Efficient Directed Model Checking

    Shahid Jabbar (University of Dortmund)
    Stefan Edelkamp (University of Dortmund)

  • Minimizing Counterexample with Pure Core Extraction and Incremental SAT

    Shengyu Shen (National University of Defense Technology)
    Ying Qin (National University of Defense Technology)
    SiKun Li (National University of Defense Technology)

20:00 Social dinner

Wednesday, January 19, 2005

8:30 - 9:00 Coffee
9:00 - 10:30 Invited Tutorial (Session Chair: Lenore Zuck)
  • Sriram K. Rajamani (Microsoft Research, Redmond, USA)
    Model Checking, Abstraction and Symbolic Execution for Software
10:30 - 11:00 Coffee
11:00 - 12:30 Applied Abstract Interpretation (Session Chair: Warren Hunt)
  • Verification of an Error Correcting Code by Abstract Interpretation

    Charles Hymans (École Polytechnique)

  • Information Flow Analysis for Java Bytecode

    Samir Genaim (University of Verona)
    Fausto Spoto (University of Verona)

  • Cryptographic protocol analysis on real C code

    Jean Goubault-Larrecq (LSV, Cachan)
    Fabrice Parrennes (RATP)

12:30 - 14:00 Lunch
14:00 - 15:00 Bounded Model Checking (Session Chair: Francesco Ranzato)
  • Optimizing Bounded Model Checking for Linear Hybrid System

    Erika Abraham (Albert-Ludwigs-Universitaet Freiburg),
    Bernd Becker (Albert-Ludwigs-Universitaet Freiburg),
    Felix Klaedtke (ETH Zuerich),
    Martin Steffen (Christian-Albrechts-Universitaet zu Kiel)

  • Simple is Better: Efficient Bounded Model Checking for Past LTL

    Timo Latvala (Helsinki University of Technology)
    Armin Biere (ETH Zurich - Computer Systems Institute)
    Keijo Heljanko (Helsinki University of Technology
    Tommi Junttila (Helsinki University of Technology)

15:00 - 15:30 Coffee
15:30 - 17:30 Verification II (Session Chair: David Monniaux)
  • Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives

    Stephen Siegel (University of Massachusetts Amherst)

  • Verifying Set Interfaces based on Object Field Values

    Patrick Lam (MIT)
    Viktor Kuncak (MIT)
    Martin Rinard (MIT)

  • On the Complexity of Error Explanation

    Nirman Kumar (Oracle Corporation)
    Viraj Kumar (University of Illinois at Urbana-Champaign)
    Mahesh Viswanathan (University of Illinois at Urbana-Champaign)

  • Efficiently Verifiable Conditions for Deadlock-freedom of Large Concurrent Programs

    Paul Attie (Northeastern University)
    Hana Chockler (Worcester Polytechnic Institute)

Thursday, January 20, 2005
Industrial Day : Automatic Tools for Verification

Friday, January 21, 2005
Aiool : 1st International Workshop on Abstract Interpretation of Object-Oriented Languages

Friday, January 21, 2005
NSAD : International Workshop on Numerical & Symbolic Abstract Domains


Panoram de Paris 360

Contact: Radhia[point]Cousot[arobase]polytechnique [point]fr
Last modified: Sunday May 23, 2010
Valid XHTML 1.1! Valid CSS!
ACM

VMCAI'05

Conference venue Invited speakers Invited tutorial Program Call for papers Committees Registration Sponsors Publication LNCS 3385

Affiliated events

Industrial Day NSAD'05 AIOOL'05

Paris

Accommodations Subway (map, itinary,...) Weather Maps

Links

VMCAI'04VMCAI'03
EAPLS