Verification, model; checking, and abstract interpretation. 3rd international workshop, VMCAI 2002, Venice, Italy, January 21--22, 2002. Revised papers (Q1604007)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Focardi, Riccardo; Piazza, Carla; Rossi, Sabina}, Proofs methods for bisimulation based information flow security, 16-31 [Zbl 1057.68065] \textit{Barthe, Gilles; Dufay, Guillaume; Jakubiec, Line; Melo de Sousa, Simão}, A formal correspondence between offensive and defensive JavaCard virtual machines, 32-45 [Zbl 1057.68571] \textit{Shyamasundar, R. K.}, Analyzing cryptographic protocols in a reactive framework, 46-64 [Zbl 1057.68615] \textit{Tan, Li}, An abstract schema for equivalence-checking games, 65-78 [Zbl 1057.68072] \textit{Sidorova, Natalia; Steffen, Martin}, Synchronous closing of timed SDL systems for model checking, 79-93 [Zbl 1057.68634] \textit{Faella, Marco; La Torre, Salvatore; Murano, Aniello}, Automata-theoretic decision of timed games, 94-108 [Zbl 1057.68057] \textit{Charatonik, Witold; Mukhopadhyay, Supratik; Podelski, Andreas}, Compositional termination analysis of symbolic forward analysis, 109-125 [Zbl 1057.68622] \textit{Genaim, Samir; Codish, Michael; Gallagher, John; Lagoon, Vitaly}, Combining norms to prove termination, 126-138 [Zbl 1057.68585] \textit{Murawski, Andrzej S.; Yi, Kwangkeun}, Static monotonicity analysis for \(\lambda\)-definable functions over lattices, 139-153 [Zbl 1057.68577] \textit{Hill, Patricia M.; Spoto, Fausto}, A refinement of the escape property, 154-166 [Zbl 1057.68586] \textit{Tronçon, Remko; Bruynooghe, Maurice; Janssens, Gerda; Catthoor, Francky}, Storage size reduction by in-place mapping of arrays, 167-181 [Zbl 1057.68597] \textit{Krstic, Sava; Matthews, John}, Verifying BDD algorithms through monadic interpretation, 182-195 [Zbl 1057.68629] \textit{Cimatti, Alessandro; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto}, Improving the encoding of LTL model checking into SAT, 196-207 [Zbl 1057.68056] \textit{Zuck, Lenore; Pnueli, Amir; Kesten, Yonit}, Automatic verification of probabilistic free choice, 208-224 [Zbl 1057.68644] \textit{Gori, Roberta; Levi, Giorgio}, An experiment in type inference and verification by abstract interpretation, 225-239 [Zbl 1057.68576] \textit{La Torre, Salvatore; Murano, Aniello; Napoli, Margherita}, Weak Muller acceptance conditions for tree automata, 240-254 [Zbl 1057.68049] \textit{Coppo, Mario; Dezani-Ciancaglini, Mariangiola}, A fully abstract model for higher-order mobile ambients, 255-271 [Zbl 1057.68640] \textit{Tiplea, Ferucio Laurentiu; Tiplea, Aurora}, A simulation preorder for abstraction of reactive systems, 272-288 [Zbl 1057.68073] \textit{Harding, Aidan; Ryan, Mark; Schobbens, Pierre-Yves}, Approximating ATL\(^*\) in ATL, 289-301 [Zbl 1057.68059] \textit{Huth, Michael}, Model checking modal transition systems using Kripke structures, 302-316 [Zbl 1057.68066] \textit{Baukus, Kai; Lakhnech, Yassine; Stahl, Karsten}, Parameterized verification of a cache coherence protocol: Safety and liveness, 317-330 [Zbl 1057.68620]