|
|
Verification, Model Checking and Abstract Interpretation |
|
|
|
|
|
|
|
|
|
Final Program Sunday, 11. 01.2004 Session Chair: Giorgio Levi 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 Boolean Algebra of Shape
Analysis Constraints, Viktor Kuncak and Martin
Rinard 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 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, Widening Operators for
Powerset Domains, Roberto Bagnara, Patricia M.
Hill, and Enea Zaffanella
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 Tuesday 13.01.2004 Session Chair: Tino Cortesi Automatic Inference of
Class Invariants, Francesco Logozzo 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 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 Session Chair: Bernhard Steffen |