TY  - BOOK
AU  - Halbwachs,Nicolas
AU  - Zuck,Lenore D.
ED  - TACAS (Conference)
ED  - ETAPS (Conference)
TI  - Tools and algorithms for the construction and analysis of systems: 11th international conference, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005 : proceedings 
T2  - Lecture notes in computer science
SN  - 9783540319801
AV  - QA76.9.S88 T33 2005
U1  - 005.1 22
PY  - 2005///
CY  - Berlin, New York
PB  - Springer
KW  - System design
KW  - Congresses
KW  - Computer software
KW  - Development
KW  - Conception de systèmes
KW  - Congrès
KW  - Logiciels
KW  - Développement
KW  - COMPUTERS
KW  - Programming
KW  - Open Source
KW  - bisacsh
KW  - Software Development & Engineering
KW  - Tools
KW  - General
KW  - Informatique
KW  - eclas
KW  - fast
KW  - Automatisches Beweisverfahren
KW  - gnd
KW  - Model Checking
KW  - Programmverifikation
KW  - Softwareentwicklung
KW  - Softwarespezifikation
KW  - Systementwicklung
KW  - Edinburgh (2005)
KW  - swd
KW  - algoritmen
KW  - algorithms
KW  - computeranalyse
KW  - computer analysis
KW  - computerwetenschappen
KW  - computer sciences
KW  - computernetwerken
KW  - computer networks
KW  - software engineering
KW  - Information and Communication Technology (General)
KW  - Informatie- en communicatietechnologie (algemeen)
KW  - Congress
KW  - Conference papers and proceedings
KW  - lcgft
KW  - Actes de congrès
KW  - rvmgf
KW  - Kongress
N1  - Includes bibliographical references and index; Invited Paper -- Applications of Craig Interpolants in Model Checking -- Regular Model-Checking -- Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking -- Simulation-Based Iteration of Tree Transducers -- Using Language Inference to Verify Omega-Regular Properties -- Infinite 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 Refinement -- Abstract 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 Understanding -- Automata and Logics -- A Note on On-the-Fly Verification Algorithms -- Truly On-the-Fly LTL Model Checking -- Complementation Constructions for Nondeterministic Automata on Infinite Words -- Using BDDs to Decide CTL -- Probabilistic Systems, Probabilistic Model-Checking -- Model Checking Infinite-State Markov Chains -- Algorithmic Verification of Recursive Probabilistic State Machines -- Monte Carlo Model Checking -- Satisfiability -- Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit -- Bounded Validity Checking of Interval Duration Logic -- An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic -- A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover -- Testing -- Symbolic Test Selection Based on Approximate Analysis -- Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution -- Abstraction and Reduction -- Dynamic Symmetry Reduction -- Localization and Register Sharing for Predicate Abstraction -- On Some Transformation Invariants Under Retiming and Resynthesis -- Specification, Program Synthesis -- Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs -- Temporal Logic for Scenario-Based Specifications -- Mining Temporal Specifications for Error Detection -- A New Algorithm for Strategy Synthesis in LTL Games -- Model-Checking -- Shortest Counterexamples for Symbolic Model Checking of LTL with Past -- Snapshot Verification -- Time-Efficient Model Checking with Magnetic Disk -- Tool Presentations -- jMoped: A Java Bytecode Checker Based on Moped -- Java-MOP: A Monitoring Oriented Programming Environment for Java -- JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP -- jETI: A Tool for Remote Tool Integration -- FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs -- SATABS: SAT-Based Predicate Abstraction for ANSI-C -- DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems -- BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking; Available to OhioLINK libraries
N2  - "This volume contains the proceedings of the 11th TACAS, International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005 took place in Edinburgh, UK, April 4-8, 2005."
UR  - https://link.springer.com/10.1007/b107194
ER  -