This book constitutes the proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, held in Macao, China, in October 2009.
The 23 regular papers and 3 took papers presented together with 3 invited talks, were carefully reviewed and selected from 74 research papers and 10 tool papers submissions.
The papers are organized in topical sections on state space reduction, tools, probabilistic systems, medley, temporal logic, abstraction and refinement, and fault tolerant systems.
Author(s): Mark R. Greenstreet (auth.), Zhiming Liu, Anders P. Ravn (eds.)
Series: Lecture Notes in Computer Science 5799 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2009
Language: English
Pages: 414
Tags: Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Algorithm Analysis and Problem Complexity; Programming Techniques; Programming Languages, Compilers, Interpreters; Software Engineering
Front Matter....Pages -
Verifying VLSI Circuits....Pages 1-20
3-Valued Abstraction for (Bounded) Model Checking....Pages 21-21
Local Search in Model Checking....Pages 22-38
Exploring the Scope for Partial Order Reduction....Pages 39-53
State Space Reduction of Linear Processes Using Control Flow Reconstruction....Pages 54-68
A Data Symmetry Reduction Technique for Temporal-epistemic Logic....Pages 69-83
TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets....Pages 84-89
CLAN: A Tool for Contract Analysis and Conflict Discovery....Pages 90-96
UnitCheck: Unit Testing and Model Checking Combined....Pages 97-103
LTL Model Checking of Time-Inhomogeneous Markov Chains....Pages 104-119
Statistical Model Checking Using Perfect Simulation....Pages 120-134
Quantitative Analysis under Fairness Constraints....Pages 135-150
A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems....Pages 151-165
Memory Usage Verification Using Hip/Sleek....Pages 166-181
Solving Parity Games in Practice....Pages 182-196
Automated Analysis of Data-Dependent Programs with Dynamic Memory....Pages 197-212
On-the-fly Emptiness Check of Transition-Based Streett Automata....Pages 213-227
On Minimal Odd Rankings for Büchi Complementation....Pages 228-243
Specification Languages for Stutter-Invariant Regular Properties....Pages 244-254
Incremental False Path Elimination for Static Software Analysis....Pages 255-270
A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement....Pages 271-288
Don’t Know for Multi-valued Systems....Pages 289-305
Logahedra: A New Weakly Relational Domain....Pages 306-320
Synthesis of Fault-Tolerant Distributed Systems....Pages 321-336
Formal Verification for High-Assurance Behavioral Synthesis....Pages 337-351
Dynamic Observers for the Synthesis of Opaque Systems....Pages 352-367
Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation....Pages 368-381
LTL Model Checking for Recursive Programs....Pages 382-396
On Detecting Regular Predicates in Distributed Systems....Pages 397-411
Back Matter....Pages -
