VMCAI 2004

26 papers

1. A Complete Method for the Synthesis of Linear Ranking Functions · Andreas Podelski, Andrey Rybalchenko
2. A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal · David Harel
3. Analysis of Recursive Game Graphs Using Data Flow Equations · Kousha Etessami
4. Applying Jlint to Space Exploration Software · Cyrille Artho, Klaus Havelund
5. Approximate Probabilistic Model Checking · Thomas Hérault, Richard Lassaigne, Frédéric Magniette, Sylvain Peyronnet
6. Automatic Inference of Class Invariants · Francesco Logozzo
7. Boolean Algebra of Shape Analysis Constraints · Viktor Kuncak, Martin C. Rinard
8. Certifying Temporal Properties for Compiled C Programs · Songtao Xia, James Hook
9. Checking Interval Based Properties for Reactive Systems · Yu Pei, Qiwen Xu
10. Completeness and Complexity of Bounded Model Checking · Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
11. Constructing Quantified Invariants via Predicate Abstraction · Shuvendu K. Lahiri, Randal E. Bryant
12. Construction of a Semantic Model for a Typed Assembly Language · Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu
13. History-Dependent Scheduling for Cryptographic Processes · Vincent Vanackère
14. Liveness with Invisible Ranking · Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
15. Model Checking Polygonal Differential Inclusions Using Invariance Kernels · Gordon J. Pace, Gerardo Schneider
16. Model Checking for Object Specifications in Hidden Algebra · Dorel Lucanu, Gabriel Ciobanu
17. On the Expressive Power of Canonical Abstraction · Shmuel Sagiv
18. Rule-Based Runtime Verification · Howard Barringer, Allen Goldberg, Klaus Havelund, Koushik Sen
19. Security Types Preserving Compilation: (Extended Abstract) · Gilles Barthe, Amitabh Basu, Tamara Rezk
20. Security, Protocols, and Trust · Joshua D. Guttman
21. Static Analysis versus Software Model Checking for Bug Finding · Dawson R. Engler, Madanlal Musuvathi
22. Symbolic Implementation of the Best Transformer · Thomas W. Reps, Shmuel Sagiv, Greta Yorsh
23. Type Inference for Parameterized Race-Free Java · Rahul Agarwal, Scott D. Stoller
24. Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking · John Hatcliff, Robby, Matthew B. Dwyer
25. Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone · Reinhard Wilhelm
26. Widening Operators for Powerset Domains · Roberto Bagnara, Patricia M. Hill, Enea Zaffanella