Automated Technology for Verification and Analysis: 5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings

Nathan Whitehead, Jordan Johnson, Martín Abadi (auth.), Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura (eds.)3540755950, 9783540755951

This book constitutes the refereed proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007, held in Tokyo, Japan, October 22-25, 2007.The 29 revised full papers presented together with 7 short papers were carefully reviewed and selected from 88 submissions. The papers address theoretical methods to achieve correct software or hardware systems, including both functional and non functional aspects; as well as applications of theory in engineering methods and particular domains and handling of practical problems occurring in tools.

---

Table of contents :
Front Matter….Pages –
Policies and Proofs for Code Auditing….Pages 1-14
Recent Trend in Industry and Expectation to DA Research….Pages 15-16
Toward Property-Driven Abstraction for Heap Manipulating Programs….Pages 17-18
Branching vs. Linear Time: Semantical Perspective….Pages 19-34
Mind the Shapes: Abstraction Refinement Via Topology Invariants….Pages 35-50
Complete SAT-Based Model Checking for Context-Free Processes….Pages 51-65
Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver….Pages 66-81
Model Checking Contracts – A Case Study….Pages 82-97
On the Efficient Computation of the Minimal Coverability Set for Petri Nets….Pages 98-113
Analog/Mixed-Signal Circuit Verification Using Models Generated from Simulation Traces….Pages 114-128
Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL Descriptions….Pages 129-144
Proving Termination of Tree Manipulating Programs….Pages 145-161
Symbolic Fault Tree Analysis for Reactive Systems….Pages 162-176
Computing Game Values for Crash Games….Pages 177-191
Timed Control with Observation Based and Stuttering Invariant Strategies….Pages 192-206
Deciding Simulations on Probabilistic Automata….Pages 207-222
Mechanizing the Powerset Construction for Restricted Classes of ω -Automata….Pages 223-236
Verifying Heap-Manipulating Programs in an SMT Framework….Pages 237-252
A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies….Pages 253-267
Distributed Synthesis for Alternating-Time Logics….Pages 268-283
Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems….Pages 284-299
Efficient Approximate Verification of Promela Models Via Symmetry Markers….Pages 300-315
Latticed Simulation Relations and Games….Pages 316-330
Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking….Pages 331-346
Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS….Pages 347-361
Continuous Petri Nets: Expressive Power and Decidability Issues….Pages 362-377
Quantifying the Discord: Order Discrepancies in Message Sequence Charts….Pages 378-393
A Formal Methodology to Test Complex Heterogeneous Systems….Pages 394-409
A New Approach to Bounded Model Checking for Branching Time Logics….Pages 410-424
Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space….Pages 425-440
A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains….Pages 441-456
3-Valued Circuit SAT for STE with Automatic Refinement….Pages 457-473
Bounded Synthesis….Pages 474-488
Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances….Pages 489-500
A Brief Introduction to $mathcal{THOTL}$ ….Pages 501-510
On-the-Fly Model Checking of Fair Non-repudiation Protocols….Pages 511-522
Model Checking Bounded Prioritized Time Petri Nets….Pages 523-532
Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications….Pages 533-542
Pruning State Spaces with Extended Beam Search….Pages 543-552
Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction….Pages 553-563
Back Matter….Pages –