Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings

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 -