search for books and compare prices
Tables of Contents for Verification, Model Checking, and Abstract Interpretation
Chapter/Section Title
Page #
Page Count
Security and Protocols
Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode
Cinzia Bernardeschi Nicoletta De Francesco
1
15
Proofs Methods for Bisimulation Based Information Flow Security
Riccardo Focardi Carla Piazza Sabina Rossi
16
16
A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines
Gilles Barthe Guillaume Dufay Line Jakubiec Simao Melo de Sousa
32
14
Analyzing Cryptographic Protocols in a Reactive Framework
R. K. Shyamasundar
46
19
Timed Systems and Games
An Abstract Schema for Equivalence-Checking Games
Li Tan
65
14
Synchronous Closing of Timed SDL Systems for Model Checking
Natalia Sidorova Martin Steffen
79
15
Automata-Theoretic Decision of Timed Games
Marco Faella Salvatore La Torre Aniello Murano
94
15
Static Analysis
Compositional Termination Analysis of Symbolic Forward Analysis
Witold Charatonik Supratik Mukhopadhyay Andreas Podelski
109
17
Combining Norms to Prove Termination
Samir Genaim Michael Codish John Gallagher Vitaly Lagoon
126
13
Static Monotonicity Analysis for λ-definable Functions over Lattices
Andrzej S. Murawski Kwangkeun Yi
139
15
A Refinement of the Escape Property
Patricia M. Hill Fausto Spoto
154
13
Optimizations
Storage Size Reduction by In-place Mapping of Arrays
Remko Troncon Maurice Bruynooghe Gerda Janssens Francky Cathoor
167
15
Verifying BDD Algorithms through Monadic Interpretation
Sava Krstic John Mathews
182
14
Improving the Encoding of LTL Model Checking into SAT
Alessandro Cimatti Marco Pistore Marco Roveri Roberto Sebastiani
196
12
Types and Verification
Automatic Verification of Probabilistic Free Choice
Lenore Zuck Amir Pnueli Yonit Kesten
208
17
An Experiment in Type Inference and Verification by Abstract Interpretation
Roberta Gori Giorgio Levi
225
15
Weak Muller Acceptance Conditions for Tree Automata
Salvatore La Torre Aniello Murano Margherita Napoli
240
15
A Fully Abstract Model for Higher-Order Mobile Ambients
Mario Coppo Mariangiola Dezani-Ciancaglini
255
17
Temporal Logics and Systems
A Simulation Preorder for Abstraction of Reactive Systems
Ferucio Laurentiu Tiplea Aurora Tiplea
272
17
Approximating ATL* in ATL
Aidan Harding Mark Ryan Pierre-Yves Schobbens
289
13
Model Checking Modal Transition Systems Using Kripke Structures
Michael Huth
302
15
Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness
Kai Baukus Yassine Lakhnech Karsten Stahl
317
14
Author Index
331
<