Tools and Algorithms for the Construction and Analysis of Systems. 17th International Conference, TACAS 2011 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 Saarbrücken, Germany, March 26–April 3, 2011 Proceedings

Cover
Lecture Notes in Computer Science 6605
Tools and Algorithms
for the Construction
and Analysis of Systems
ISBN 9783642198342
Foreword
Preface
Conference Organization
Table of Contents
Reliable Software Development: Analysis-Aware Design
	References
Transition Invariants and Transition Predicate Abstraction for Program Termination
	Introduction
	Preliminaries
	Disjunctively Well-Founded Transition Invariants
	Transition Predicate Abstraction (TPA)
	Conclusion
	References
Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
	Introduction
	Preliminaries
		Programming Model
	Operational Memory Models
	Violations of Sequential Consistency
		Execution Traces
		Sequential Consistency and the Happens-Before Relation
	Monitoring Algorithms
	Comparison to SOBER
	Experimental Evaluation
	References
Compositionality Entails Sequentializability
	Introduction
	A Compositional Abstract Semantics for Programs
	A High Level Overview of the Sequentialization
	Sequential and Concurrent Programs
	The Sequentialization
	Experience
	Future Directions
	References
Litmus: Running Tests against Hardware
	Introduction
	High Level Overview
	Test Infrastructure and Parameters
	The Impact of Test Parameters
	References
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
	Introduction
	Ground AC-Completion
	Shostak Theories and Global Canonization
	Ground AC-Completion Modulo X
		Canonized Rewriting
		The AC(X) Algorithm
	Correctness
		Soundness
		Completeness
		Termination
	Experimental Results
	Conclusion and Future Works
	References
Invariant Generation in Vampire
	Introduction
	Invariant Generation in Vampire: Overview
	Conclusion
	References
Enforcing Structural Invariants Using Dynamic Frames
	Introduction
	Dynamic Frames
		Inferring Regions Automatically
	Verifiably Acyclic Data Structures
		A Characterization of acyclicity
		Preserving the Acyclicity Invariant
	Trees and Similar Data Structures
	Improving Precision
	Evaluation
	Related Work
	Conclusions
	References
Loop Summarization and Termination Analysis
	Introduction
	Background
		Termination
		Loop Summarization
	Loop Summarization with Transition Invariants
	Selection of Candidate Invariants
	Evaluation
	Related Work
		Relation to Size-Change Termination Principle
		Relation to Other Research Using Transition Invariants
	Conclusion and Future Work
	References
Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata
	Introduction
	A Model of Open Timed Automata with Inputs/Outputs
		Open Timed Automata with Inputs/Outputs
		The Semantics of OTAIOs
		Properties and Operations
	Conformance Testing Theory
		The tioco Conformance Theory
		Refinement Preserving tioco
	Approximate Determinization Preserving tioco
		A Game Approach to Determinize Timed Automata
		Extensions to TAIOs and Adaptation to tioco
	Off-Line Test Case Generation
		Test Purposes
		Principle of Test Generation
	Conclusion
	References
Quantitative Multi-objective Verification for Probabilistic Systems
	Introduction
	Background
		Probabilistic Automata (PAs)
		Verification of PAs
	Quantitative Multi-objective Verification
		Checking Multi-objective Queries
		Controller Synthesis
	Quantitative Assume-Guarantee Verification
	Conclusions
	References
Efficient CTMC Model Checking of Linear Real-Time Objectives
	Introduction
	Preliminaries
		Continuous-Time Markov Chains
		Deterministic Timed Automata
		Decomposition for 1-Clock DTA
	Lumping
	Experimental Results
		Cyclic Polling Server
		Robot Navigation
		Systems Biology
		Parallelization
	Multi-clock DTA Objectives
	Conclusion
	References
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
	Motivations, Related Work and Goals
	Background: SMT(LA(Z))
		Generalities
		Efficient SMT(LA(Z)) Solving
	From LA(Z)-Solving to LA(Z)-Interpolation
		Interpolation for Diophantine Equations
		Interpolation for Inequalities
		Interpolation with Branch-and-Bound
	A Novel General Interpolation Technique for Inequalities
	Experimental Evaluation
		Description of the Benchmark Sets
		Comparison with the State-of-the-Art Tools Available
	Conclusions
	References
Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems
	Introduction
	Stochastic Boolean Satisfiability
	Resolution for SSAT
	Interpolation for SSAT
		Generalized Craig Interpolants
		Computation of Generalized Craig Interpolants
	Interpolation-Based Probabilistic Model Checking
	Conclusion and Future Work
	References
Specification-Based Program Repair Using SAT
	Introduction
	Basic Principle
	Our Framework
	Evaluation
		Candidates
		Metrics
		Results
	Discussion
	Correctness Argument
	Related Work
		Program Sketching Using SAT
		Program Repair Using Data Structure Repair
		Other Recent Work on Program Correction
	Conclusion
	References
Optimal Base Encodings for Pseudo-Boolean Constraints
	Introduction
	Optimal Base Problems
	Encoding Pseudo-Boolean Constraints
	Measures of Optimality
	Optimal Base Search I: Heuristic Pruning
	Optimal Base Search II: Branch and Bound
	Optimal Base Search III: Search Modulo Product
	Experiments
	Related Work
	Conclusion
	References
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
	Introduction
	Preliminaries
	Inferring Loop Invariants with Algorithmic Learning
	Predicate Generation by Interpolation
		Initial Atomic Predicates
		Atomic Predicates from Incorrect Conjectures
		Atomic Predicates from Conflicting Abstract Counterexamples
	Algorithm
	Experimental Results
		tar from Tar
		parser from SPEC2000 Benchmarks
	Conclusions
	References
Next Generation LearnLib
	Introduction
	Base Technology
	Modeling Learning Solutions
	Fast-Cycle Experimentation: The ZULU Experience
	Conclusion
	References
Applying CEGAR to the Petri Net State Equation
	Introduction
	The Reachability Problem
	Traversing the Solution Space
	Building Constraints
	Finding Partial Solutions
	Experimental Results
	Conclusion
	References
Biased Model Checking Using Flows
	Introduction
		Applications to Distributed Message Passing Protocols
		Evaluation
	Related Work
	Preliminaries
	Biased BFS Algorithm
		Optimizations
	Biased DFS Algorithm
	Flows and Markings
	Experimental Evaluation
		Results
		Biased Procedures in Murphi
		Discussion
	Conclusion
	References
S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems
	Introduction
	The S-TaLiRo Tool
	Usage
	Related Work
	References
GAVS+: An Open Platform for the Research of Algorithmic Game Solving
	Introduction
	Supported Games in GAVS+
	Extension of Strips/PDDL for Game Solving: An Example
	References
Büchi Store: An Open Repository of Büchi Automata
	Introduction
	Implementation and Main Features
	Use Cases
	References
QUASY: Quantitative Synthesis Tool
	Introduction
	Synthesis from Combined Specifications
	Implementation Details
	Future Work
	References
Unbeast: Symbolic Bounded Synthesis
	Introduction
	Tool Description
		Technology
	Experimental Results
	Conclusion
	References
Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy
	Introduction
	Preliminaries
		Notation
		Directed Model Checking
		Pattern Database Heuristics
	Pattern Selection Based on Downward Refinement
		Sufficiently Accurate Distance Heuristics
		Concretizable Traces and Safe Abstractions
		An Algorithm for Pattern Selection Based on Downward Refinement
	Related Work
	Evaluation
		Implementation Details
		Experimental Setup
		Experimental Results
		Directed Model Checking for Correct Systems?
	Conclusions
	References
The ACL2 Sedan Theorem Proving System
	Introduction
	Termination Analysis Using Calling Context Graphs
	Random Testing and Proving: Synergistic Combination
	References
On Probabilistic Parallel Programs with Process Creation and Synchronisation
	Introduction
	Preliminaries
	Results
		Relationship with Probabilistic Pushdown Systems (pPDSs)
		Probability of Termination
		Probability of Finite Space
		Work and Time
	Case Studies
		Divide and Conquer
		Evaluation of Game Trees
	Conclusions and Future Work
	References
Confluence Reduction for Probabilistic Systems
	Introduction
	Preliminaries
		Probability Theory and Probabilistic Automata
		Schedulers
	Branching Probabilistic Bisimulation
		Weak Steps for Probabilistic Automata
		Branching Probabilistic Bisimulation
	Confluence for Probabilistic Automata
	State Space Reduction Using Probabilistic Confluence
	Symbolic Detection of Probabilistic Confluence
	Case Study
	Conclusions
	References
Model Repair for Probabilistic Systems
	Introduction
	Parametric Probabilistic Model Checking
	The Model Repair Problem
		The Max-Profit Model Repair Problem
	Model Repair as a Nonlinear Programming Problem
	Model Repair Feasibility and Optimality
	Model Repair and Optimal Control
	Applications
	Related Work
	Conclusions
	References
Boosting Lazy Abstraction for SystemC with Partial Order Reduction
	Introduction
	Background
	The Problem of Multiple Interleavings
	Reduction Algorithms in ESST
		Partial-Order Reduction Techniques
		Applying POR to ESST
		Correctness of Reduction in ESST
	Related Work
	Experiments
	Conclusion and Future Work
	References
Modelling and Verification of Web Services Business Activity Protocol
	Introduction
	WS-Business Activity Protocol
		Business Agreement with Coordination Completion
		Communication Policies
	Formal Modelling of BAwCC in UPPAAL
	Analysis of BAwCC
	Enhanced BAwCC
	Termination under Fairness
	Conclusion and Future Work
	References
CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
	Introduction
	Architecture and Verification Technology
	Specification Languages
		Support for the LOTOS Language
		Support for the FSP Language
		Support for the LOTOS NT Language
		Support for Other Languages
	Model Checking
	Equivalence Checking
	Performance Evaluation
	Parallel and Distributed Methods
	Conclusion
	References
GameTime: A Toolkit for Timing Analysis of Software
	Introduction
	Running Example
	The GameTime Approach
		Generating Basis Paths
		Sample Experimental Result
	References
Author Index