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.
Author(s): Nathan Whitehead, Jordan Johnson, Martín Abadi (auth.), Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura (eds.)
Series: Lecture Notes in Computer Science 4762
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2007
Language: English
Pages: 570
Tags: Logics and Meanings of Programs; Information Systems and Communication Service; Computer Communication Networks; Special Purpose and Application-Based Systems; Software Engineering; Programming Languages, Compilers, Interpreters
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 -
