VMCAI 2002

22 papers

1. A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines · Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa
2. A Fully Abstract Model for Higher-Order Mobile Ambients · Mario Coppo, Mariangiola Dezani-Ciancaglini
3. A Refinement of the Escape Property · Patricia M. Hill, Fausto Spoto
4. A Simulation Preorder for Abstraction of Reactive Systems · Ferucio Laurentiu Tiplea, Aurora Tiplea
5. An Abstract Schema for Equivalence-Checking Games · Li Tan
6. An Experiment in Type Inference and Verification by Abstract Interpretation · Roberta Gori, Giorgio Levi
7. Analyzing Cryptographic Protocols in a Reactive Framework · R. K. Shyamasundar
8. Approximating ATL* in ATL · Aidan Harding, Mark Ryan, Pierre-Yves Schobbens
9. Automata-Theoretic Decision of Timed Games · Marco Faella, Salvatore La Torre, Aniello Murano
10. Automatic Verification of Probabilistic Free Choice · Lenore D. Zuck, Amir Pnueli, Yonit Kesten
11. Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode · Cinzia Bernardeschi, Nicoletta De Francesco
12. Combining Norms to Prove Termination · Samir Genaim, Michael Codish, John P. Gallagher, Vitaly Lagoon
13. Compositional Termination Analysis of Symbolic Forward Analysis · Witold Charatonik, Supratik Mukhopadhyay, Andreas Podelski
14. Improving the Encoding of LTL Model Checking into SAT · Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani
15. Model Checking Modal Transition Systems Using Kripke Structures · Michael Huth
16. Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness · Kai Baukus, Yassine Lakhnech, Karsten Stahl
17. Proofs Methods for Bisimulation Based Information Flow Security · Riccardo Focardi, Carla Piazza, Sabina Rossi
18. Static Monotonicity Analysis for lambda-definable Functions over Lattices · Andrzej S. Murawski, Kwangkeun Yi
19. Storage Size Reduction by In-place Mapping of Arrays · Remko Tronçon, Maurice Bruynooghe, Gerda Janssens, Francky Catthoor
20. Synchronous Closing of Timed SDL Systems for Model Checking · Natalia Sidorova, Martin Steffen
21. Verifying BDD Algorithms through Monadic Interpretation · Sava Krstic, John Matthews
22. Weak Muller Acceptance Conditions for Tree Automata · Salvatore La Torre, Aniello Murano, Margherita Napoli