Fifth International Conference on

Verification, Model Checking and Abstract Interpretation

 

 

 

 

 

 

Final Program

Sunday, 11. 01.2004

 

13:30 Registration

 

Session Chair: Giorgio Levi

 

14:00 - 15:30 Tutorial: Joshua Guttman

 

15:30 - 16:00 Coffee break

 

16:00- 18:00 Security and Formal Methods

 

Security Types Preserving Compilation, Gilles Barthe, Amitabh Basu, and Tamara Rezk

 

History-Dependent Scheduling for Cryptographic Processes,Vincent Vanackere

 

Construction of a Semantic Model for a Typed Assembly Language , Gang Tan, Andrew W. Appel, Kedar N. Swadi, and Dinghao Wu

 

Rule-Based Runtime Verification, Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen

 

 

Monday, 12.01.2004

 

Session Chair: David Schmidt

 

9:00 - 10:30 Invited Talk: Mooly Sagiv

 

Boolean Algebra of Shape Analysis Constraints, Viktor Kuncak and Martin Rinard

 

10:30 - 11:00 Coffee break

 

11:00 - 12:30 Model checking

 

Session Chair: Lenore Zuck

 

Approximate Probabilistic Model Checking, Thomas Herault, Richard Lassaigne, Frederic Magniette, and Sylvain Peyronnet

 

Completeness and Complexity of Bounded Model Checking, Edmund Clarke, Daniel Kroening, Joel Ouaknine, and Ofer Strichman

 

Model Checking for Object Specifications in Hidden Algebra, Dorel Lucanu and Gabriel Ciobanu

 

14:00 - 15:30 Foundations I

 

Session Chair:  Susanne Graf

 

Model Checking Polygonal Differential Inclusions Using Invariance Kernels, Gordon J. Pace and Gerardo Schneider  

 

Checking Interval Based Properties for Reactive Systems, Pei Yu and Xu Qiwen

 

Widening Operators for Powerset Domains, Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella

 

15:30 - 16:00 Coffee break

 

16:00- 17:30 Software Checking

 

Session Chair: Yassine Lakhnech

 

Type Inference for Parameterized Race-Free Java, Rahul Agarwal and Scott D. Stoller

 

Certifying Temporal Properties for Compiled C Programs, Songtao Xia and James Hook

 

Verifying Atomicity Specifications for Condurrent Object-Oriented Software using Model-Checking, John Hatcliff, Robby, and Matthew B. Dwyer

 

19:30 - ...  Banquet

 

 

Tuesday 13.01.2004

 

Session Chair: Tino Cortesi

 

9:00 - 10:30 Invited Talk: Dawson Engeler

 

Automatic Inference of Class Invariants, Francesco Logozzo

 

10:30 - 11:00 Coffee break

 

11:00 - 12:30 Liveness and Completeness

 

Session Chair: Markus Müller-Olm

 

Liveness with Invisible Ranking, Yi Fang, Nir Piterman, Amir Pnueli, and Lenore Zuck  

 

A Complete Method for Synthesis of Linear Ranking Functions, Andrey Rybalchenko and Andreas Podelski  

 

Symbolic Implementation of the Best Transformer, Tomas Reps, Mooly Sagiv, and Greta Yorsh  

 

14:00 - 15:30 Foundations II

 

Session Chair: Radhia Cousot

 

Constructing Quantified Invariants via Predicate Abstraction, Shuvendu K. Lahiri and Randal E. Bryant

 

Analysis of Recursive Game Graphs using Data Flow Equations, Kousha Etessami

 

Applying Jlint to Space Exploration Software, Cyrille Artho and Klaus Havelund

 

Why AI + ILP is good for WCET, but MC is not, nor ILP alone, Reinhard Wilhelm

 

16:00 - 16:30 Coffee break

 

Session Chair: Bernhard Steffen

 

16:30- 17:30 Key Note Speech: David Harel