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