验证与分析的自动化技术 Automated technology for verification and analysis

出版时间：2006-12  出版社：湖南文艺出版社  作者：Susanne Graf 著  页数：540  

内容概要

This book constitutes the refereed proceedings of the Third International Symposium on Automated Technology for Verificaton and Analysis, ATVA 2006, held in Beijing, China in October 2006.    The 35 revised full papers presented together with abstracts of 3 keynote papers were carefully reviewed and selected from 137 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.

书籍目录

Keynote Speeches  Analysis of Recursive Probabilistic Models  Verification Challenges and Opportunities in the New Era Of MicrOprocessOr Design  Automated Abstraction of SoftwareRegular Papers  Symmetry Reduction for Probabilistic Model Checking Using Generic Represent  Eager Markov Chains  A Probabilistic Learning Approach for Counterexample Guided  Abstraction Refinement  A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic  Reachability Analysis  Model Checking Timed Systems with Urgencies  Whodunit?Causal Analysis for Counterexamples  On the Membership Problem for Visibly Pushdown Languages  On the Construction of Fine Automata for Safety Properties  0n the Succinctness of Nondeterminism  Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains  Compositional Reasoning for Hardware/Software Co-verification  Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition  On the Satisfiability of Modular Arithmetic Formulae  Selective Approaches for Solving Weak Games  Controller Synthesis and Ordinal Automata  Effective Contraction of Timed STGs for Decomposition Based Timed Circuit Synthesis  Synthesis for Probabilistic Environments  Branching-Time Property Preservation Between Real-Time Systems  Automatic Verification of Hybrid Systems with Large Discrete State Space  Timed Unfoldings for Networks of Timed Automata  ……Author Index