The Automated Technology for Veri?cation and Analysis (ATVA) international symposium series was initiated in 2003, responding to a growing interest in formal veri?cation spurred by the booming IT industry, particularly hardware design and manufacturing in East Asia. Its purpose is to promote research on automated veri?cation and analysis in the region by providing a forum for int- action between the regional and the international research/industrial commu- ties of the ?eld. ATVA 2006, the fourth of the ATVA series, was held in Beijing, China, October 23-26, 2006. The main topics of the symposium include th- ries useful for providing designers with automated support for obtaining correct software or hardware systems, as well as the implementation of such theories in tools or their application. This year, we received a record number of papers: a total of 137 submissions from 27 countries. Each submission was assigned to three Program Comm- tee members, who could request help from subreviewers, for rigorous and fair evaluation. The ?nal deliberation by the Program Committee was conducted through Springer’s Online Conference Service for a duration of about 10 days after nearly all review reports had been collected. In the end, 35 papers were selected for inclusion in the program. ATVA 2006 had three keynote speeches given respectively by Thomas Ball, Jin Yang, and Mihalis Yannakakis. The main symposium was preceded by a tutorial day, consisting of three two-hourlectures given by the keynotespeakers.
Author(s): Mihalis Yannakakis (auth.), Susanne Graf, Wenhui Zhang (eds.)
Series: Lecture Notes in Computer Science 4218 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2006
Language: English
Pages: 546
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 -
Analysis of Recursive Probabilistic Models....Pages 1-5
Verification Challenges and Opportunities in the New Era of Microprocessor Design....Pages 6-7
Automated Abstraction of Software....Pages 8-8
Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives....Pages 9-23
Eager Markov Chains....Pages 24-38
A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement....Pages 39-50
A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis....Pages 51-66
Model Checking Timed Systems with Urgencies....Pages 67-81
Whodunit? Causal Analysis for Counterexamples....Pages 82-95
On the Membership Problem for Visibly Pushdown Languages....Pages 96-109
On the Construction of Fine Automata for Safety Properties....Pages 110-124
On the Succinctness of Nondeterminism....Pages 125-140
Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains....Pages 141-153
Compositional Reasoning for Hardware/Software Co-verification....Pages 154-169
Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition....Pages 170-185
On the Satisfiability of Modular Arithmetic Formulae....Pages 186-199
Selective Approaches for Solving Weak Games....Pages 200-214
Controller Synthesis and Ordinal Automata....Pages 215-228
Effective Contraction of Timed STGs for Decomposition Based Timed Circuit Synthesis....Pages 229-244
Synthesis for Probabilistic Environments....Pages 245-259
Branching-Time Property Preservation Between Real-Time Systems....Pages 260-275
Automatic Verification of Hybrid Systems with Large Discrete State Space....Pages 276-291
Timed Unfoldings for Networks of Timed Automata....Pages 292-306
Symbolic Unfoldings for Networks of Timed Automata....Pages 307-321
Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise....Pages 322-336
Timed Temporal Logics for Abstracting Transient States....Pages 337-351
Predicate Abstraction of Programs with Non-linear Computation....Pages 352-368
A Fresh Look at Testing for Asynchronous Communication....Pages 369-383
Proactive Leader Election in Asynchronous Shared Memory Systems....Pages 384-398
A Semantic Framework for Test Coverage....Pages 399-414
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols....Pages 415-429
Analyzing Security Protocols in Hierarchical Networks....Pages 430-445
Functional Analysis of a Real-Time Protocol for Networked Control Systems....Pages 446-460
Symbolic Semantics for the Verification of Security Properties of Mobile Petri Nets....Pages 461-476
Sigref – A Symbolic Bisimulation Tool Box....Pages 477-492
Towards a Model-Checker for Counter Systems....Pages 493-507
The Implementation of Mazurkiewicz Traces in POEM....Pages 508-522
Model-Based Tool-Chain Infrastructure for Automated Analysis of Embedded Systems....Pages 523-537
Back Matter....Pages -
