Tools and Algorithms for the Construction and系统构建与分析工具与算法/会议录

出版时间：2005-9  出版社：北京燕山出版社  作者：Halbwachs, Nicolas; Zuck, Lenore;  页数：588  

内容概要

This book constitutes the refereed proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held in Edinburgh, UK in April 2005 as part of ETAPS.    The 33 revised full research papers and 8 revised tool demonstration papers presented together with an invited paper were carefully reviewed and selected from a total of 161 submissions. The papers are organized in topical sections on regular model-checking, infinite state machines, abstract interpretation, automata and logics, probabilistic systems and probabilistic model checking, satisfiability, testing, abstraction and reduction, specification and program synthesis, and model-checking.

书籍目录

Invited Paper  Applications of Craig Interpolants in Model CheckingRegular Model-Checking  Verifying Programs with Dynamic l-Selector-Linked Structures in Regular Model Checking  Simulation-Based Iteration of Tree Transducers  Using Language Inference to Verify Omega-Regular PropertiesInfinite State Systems  On-the-Fly Reachability and Cycle Detection for Recursive State Machines  Empirically Efficient Verification for a Class of Infinite-State Systems  Context-Bounded Model Checking of Concurrent Software  A Generic Theorem Prover of CSP RefinementAbstract Interpretation  Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems  An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation  Dependent Types for Program UnderstandingAutomata and Logics  A Note on On-the-Fly Verification Algorithms Stefan Schwoon, Javier Esparza  Truly On-the-Fly LTL Model Checking  Complementation Constructions for Nondeterministic Automata on Infinite Words  Using BDDs to Decide CTLProbabilistic Systems, Probabilistic Model-Checking  Model-Checking Infinite-State Markov Chains  Algorithmic Verification of Recursive Probabilistic State Machines  Monte Carlo Model CheckingSatisfiability  Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit  Bounded Validity Checking of Interval Duration Logic  ……TestingAbstraction and ReductionSpecification,Program SynthesisModel-CheckingTool PresentationsAuthor Index