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

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