Computer Aided Verification
24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings
Published on 22. June 2012
XVI, 789 pages
978-3-642-31424-7 (ISBN)
Description
This book constitutes the refereed proceedings of the 24th International Conference on Computer Aided Verification, CAV 2012, held in Berkeley, CA, USA in July 2012. The 38 regular and 20 tool papers presented were carefully reviewed and selected from 185 submissions. The papers are organized in topical sections on automata and synthesis, inductive inference and termination, abstraction, concurrency and software verification, biology and probabilistic systems, embedded and control systems, SAT/SMT solving and SMT-based verification, timed and hybrid systems, hardware verification, security, verification and synthesis, and tool demonstration.
More details
Other editions
Additional editions
Madhusudan Parthasarathy | Sanjit A. Seshia
Computer Aided Verification
24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings
Book
06/2012
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Invited Talks
- Synthesis and Some of Its Challenges
- Model Checking Cell Biology
- Invited Tutorials
- Synthesizing Programs with Constraint Solvers
- IC3 and beyond: Incremental, Inductive Verification
- References
- Formal Verification of Genetic Circuits
- References
- From C to Infinity and Back: Unbounded Auto-active Verification with VCC
- References
- Automata and Synthesis
- Deterministic Automata for the (F,G)-Fragment of LTL
- Introduction
- Linear Temporal Logic
- Deterministic Automaton for the (F,G)-Fragment
- Muller Acceptance Condition
- Correctness
- Generalized Rabin Condition
- Rabin Condition
- Complexity
- Experimental Results and Evaluation
- Discussion on Extensions
- Conclusions
- References
- Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
- Introduction
- Definitions
- Algorithms for General Consumption Games
- Algorithms for One-Player and Decreasing Consumption Games
- The Emptiness and Membership Problems
- Minimal Safe Configurations and Multi-distance Reachability
- Computing Safe(s) in One-Player Consumption Games
- Computing Safe(s) in Decreasing Consumption Games
- Conclusions
- References
- ACTL n LTL Synthesis
- Introduction
- Preliminaries
- Translating LTL Formulas into UVWs
- The Case of Automata over Infinite Words
- Decomposing a Language over Finite Words into a Non-deterministic Very-Weak Automaton
- Reduction of the Synthesis Problem to Parity Games
- Solving Parity Games Symbolically
- Experimental Results
- Conclusion
- References
- Inductive Inference and Termination
- Learning Boolean Functions Incrementally
- Introduction
- Preliminary
- The CDNF Algorithm
- Incremental Learning
- Incremental Teacher
- The CDNF+ Algorithm
- The CDNF++ Algorithm
- Experiments
- Conclusion
- References
- Interpolants as Classifiers
- Introduction
- An Overview of the Technique
- Preliminaries
- SVM Primer
- Classification Based Algorithms for Interpolation
- Algorithm for Intersection of Half-spaces
- A Sound Algorithm
- Handling Superficial Non-linearities
- Experiments
- Related Work
- Conclusion
- References
- Termination Analysis with Algorithmic Learning
- Introduction
- Termination Analysis via Transition Invariants
- Program Termination and Transition Invariant
- Intensional Transition Invariants
- Algorithmic-Learning-Based Inference of Transition Invariants
- CDNF Learning Algorithm
- Learning Algorithm as an Inference Engine
- Algorithms for Mechanical Teacher
- Experiments
- Related Work
- Conclusion
- References
- Automated Termination Proofs for Java Programs with Cyclic Data
- Introduction
- Handling Irrelevant Cycles
- Abstract States in Termination Graphs
- Constructing the Termination Graph
- Proving Termination via Term Rewriting
- Handling Marking Algorithms on Cyclic Data
- Constructing the Termination Graph
- Proving Termination of Marking Algorithms
- Handling Algorithms with Definite Cyclicity
- Constructing the Termination Graph
- Proving Termination of Algorithms with Definite Reachability
- Experiments and Conclusion
- References
- Proving Termination of Probabilistic Programs Using Patterns
- Introduction
- Preliminaries
- Probabilistic Programs
- Patterns
- Nondeterministic Programs
- Our Algorithm
- Implementing Pattern Checkers
- Experimental Evaluation
- Conclusions
- References
- Abstraction
- The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
- Introduction
- The Gauge Abstraction
- Abstract Interpretation Framework
- The Gauge Domain
- Experimental Evaluation
- Conclusion
- References
- Diagnosing Abstraction Failure for Separation Logic-Based Analyses
- Introduction
- Separation Logic-Based Shape Analysis
- Abstraction Failure Diagnosis
- Feasibility Checking
- A Memory Model
- Encoding to SMT
- Doomed State Synthesis
- Experimental Evaluation
- Related Work
- Conclusion
- References
- A Method for Symbolic Computation of Abstract Operations
- Introduction
- Overview
- Algorithm for Assume"0365ssume[](A)
- Instantiations
- Experiments
- Applications to Other Symbolic Operations
- Related Work
- References
- Leveraging Interpolant Strength in Model Checking
- Introduction
- Preliminaries
- Craig Interpolation
- Resolution Proofs
- Strength of Interpolants
- Simultaneous Abstraction with Interpolation
- Problem Description
- Proof for Pudlák's System
- Proof Generalization
- Application to Model Checking
- Inductive Sequence of Interpolants
- Problem Description
- Proof for Pudlák's System
- Proof Generalization
- Application to Model Checking
- Related Work
- Conclusion
- References
- Concurrency and Software Verification
- Detecting Fair Non-termination in Multithreaded Programs
- Introduction
- Recursive Multithreaded Programs
- Bounded Compositional Non-termination Analysis
- Annotated Traces
- Compositional Detection of Periodic Traces
- From Thread-Periodic Traces to Sequential Reachability
- Encoding Fairness
- Reduction to Sequential Program Analysis
- Experimental Evaluation
- Related Work
- Conclusion
- References
- Lock Removal for Concurrent Trace Programs
- Introduction
- Motivation
- Lock Removal: The Core Idea
- The Lock Removal Strategy
- Conservative Static Check
- Compositional Lock Removal
- Deciding Static Reachability
- Compositional Analysis
- Identifying the Locks to Be Retained
- Applying Lock Removal to the Running Example
- Experiments
- Related Work
- Conclusions
- References
- How to Prove Algorithms Linearisable
- Introduction
- Example
- Linearisability and Refinement
- Proving Linearisability with Backward Simulation
- Backward Simulation for the Case Study
- Verification with KIV
- Related Work
- Conclusion and Future Work
- References
- Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
- Introduction
- Model Definition
- Synchronisation-Bounded Reachability
- Comparison with Context-Bounded Model Checking
- Optimisations
- Implementation and Experimental Results
- Conclusions and Future Work
- References
- Software Model Checking via IC3
- Introduction
- Background and Notation
- IC3withSMT
- Tree-Based IC3
- HybridTreeIC3
- Implementation and Experiments
- Implementation Details
- Benchmarks and Evaluation
- Results
- Related Work
- Conclusions and Future Work
- References
- Biology and Probabilistic Systems
- Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits
- Introduction
- Delayed CTMC
- Genetic Regulatory Circuits
- Specifying Genetic Regulatory Circuits
- Dynamics in Terms of Delayed CTMCs
- Comparison of Different Semantics for GRCs
- Probability Distributions for Delayed Reactions
- Examples Demonstrating Qualitatively Different Behavior
- Behavior Computation of Delayed CTMC
- Implementation and Results
- Conclusion
- References
- Assume-Guarantee Abstraction Refinement for Probabilistic Systems
- Introduction
- Preliminaries
- Counterexamples to Strong Simulation
- CEGAR for Checking Strong Simulation
- Assume-Guarantee Abstraction Refinement
- Implementation and Results
- Conclusion and Future Work
- References
- Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking
- Introduction
- Importance Sampling
- Estimators
- The Cross-Entropy Method
- A Parametrised Cross-Entropy Algorithm
- The Algorithm
- Examples
- Chemical Network
- Repair Model
- Conclusions and Future Work
- References
- Embedded and Control Systems
- Timed Relational Abstractions for Sampled Data Control Systems
- Introduction
- Sampled Data Control Systems
- Relationalization
- Dealing with Autonomous Transitions
- Experimental Evaluation
- References
- Approximately Bisimilar Symbolic Models for Digital Control Systems
- Introduction
- Systems and Approximate Equivalences
- Symbolic Models for Control Systems
- Main Construction
- Comparison with Previous Techniques
- Examples
- DC Motor
- Motion Planing
- Pendulum with Resource Constraints
- References
- Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
- Introduction
- The Application: Logica Di Sicurezza
- The Radio Block Section
- Verification Properties of the RBS
- The Velos Specification
- Verification Techniques and Tools
- Verification Approach
- From Velos Specifications to NuSMV Models
- From Velos Specifications to C Programs
- Model Checking Sequential Software with Multiple Assertions
- Experimental Evaluation
- Benchmarks
- Setup and Configurations
- Results of Experiments
- Remarks on other Experiments
- Related Work
- Conclusions and Future Work
- References
- SAT/SMT Solving and SMT-based Verification
- Minimum Satisfying Assignments for SMT
- Introduction
- Minimum Satisfying Assignments and Their Properties
- A Branch-and-Bound Algorithm for Computing MSAs
- Variable Order and Initial Cost Estimate
- Using Implicants to Approximate MSAs
- Computing Minimum T-satisfiable Monotone Implicants
- Using Implicates to Identify Non-universal Sets
- Implementation
- Experimental Results
- Other Strategies to Obtain Bound and Variable Order
- Related Work
- Conclusion
- References
- When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
- Introduction
- Preliminaries
- XOR Constraints
- Resolution Refutation and Craig Interpolation
- Satisfiability Solving under XOR Constraints
- XOR Reasoning
- Implementation Issues
- Refutation and Interpolation
- Interpolant Generation
- Implementation Issues
- Experimental Results
- Related Work
- Conclusions and Future Work
- References
- A Solver for Reachability Modulo Theories
- Introduction
- The Corral Architecture
- Stratified Inlining
- Variable Abstraction and Refinement
- Hierarchical Refinement
- Evaluation
- Evaluating Components of Corral
- SDV Benchmarks
- SV-COMP Benchmarks
- .NET Benchmarks
- Related Work
- References
- Timed and Hybrid Systems
- On Decidability of Prebisimulation for Timed Automata
- Introduction
- Timed Automata
- Semantics
- Bisimulations for Timed Systems
- Timed Performance Prebisimulation
- Zone Valuation Graph and Deciding Prebisimulation
- Zone Valuation Graph
- Decidability of Timed Performance Prebisimulation
- Generating Zone Valuation Graph
- Algorithm: Deciding Timed Performance Prebisimulation Using Zone Valuation Graph
- Conclusion and Future Work
- References
- Exercises in Nonstandard Static Analysis of Hybrid Systems
- Introduction
- Preliminaries
- A Leading Example: ETCS
- Program Simplification Strategies
- Phase Split
- From Standard to Nonstandard I: Modular Transfer
- Superfluous Guard Elimination
- Time Elapse
- Precondition/Invariant Discovery Strategies
- Invariant via Quantifier Elimination
- From Standard to Nonstandard II: The Transfer Principle and Symbolic Computation in Mathematica
- Differential Invariant
- Iteration Count
- Cast to Shadow
- Implementation and Experiments
- References
- A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
- Introduction
- Preliminaries
- Notation
- Finding Error States through Search
- Guided Search
- The Box-Based Distance Measure
- A Trajectory-Based Distance Measure
- The Box-Based Approximation
- Experiments
- Case Studies
- Experimental Results
- Conclusions
- References
- Hardware Verification
- An Axiomatic Memory Model for POWER Multiprocessors
- Introduction
- Background: The POWER Memory Model
- Subtleties of the POWER Memory Model
- The Operational Specification
- The Axiomatic Specification
- Axiomatic Candidate Executions
- Overview of the Specification
- Examples
- Formal Specification
- Experimental Validation
- Proof of Equivalence to the Operational Specification
- Operational to Axiomatic
- Axiomatic to Operational
- Evaluating the Axiomatic Specification with a SAT Solver
- References
- nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces
- Introduction
- The BackSpace Framework
- Background
- Trace Buffers
- Abstraction
- Semi-Thue Systems
- nuTAB-BackSpace
- Formalizing the Intuition
- Algorithm
- Correctness
- Experiments
- Simulation-Based Evaluation
- Case Study: The Leon3 SoC Hardware Prototype
- Conclusion and Future Work
- References
- Incremental, Inductive CTL Model Checking
- Introduction
- Preliminaries
- Algorithm
- An Outline of IICTL
- Forall-Exists Generalization
- Refinements
- Fairness
- Results
- Conclusion
- References
- Security
- Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
- Introduction
- Overview
- Technical Description
- Runtime Checks for Safety Properties
- JavaScript Prototype
- Experimental Evaluation
- Results
- Related Work
- References
- Automatic Quantification of Cache Side-Channels
- Introduction
- Preliminaries
- Quantifying Information Leaks
- Static Analysis of Channels
- Cache Channels
- Caches
- Two Adversary Models Observing the Cache
- Abstract Domains for Cache Analysis
- Counting Cache States
- Concrete States Respecting may
- Concrete States Respecting must
- Concrete States Respecting must and may
- Counting for Probing Adversaries
- Case Study
- Tool Support
- Target Implementations
- Improving Precision by Partitioning
- Results and Security Interpretation
- Prior Art
- Conclusions and Future Work
- References
- Secure Programming via Visibly Pushdown Safety Games
- Introduction
- Overview
- An Example Policy-Weaving Problem: Filter on MiniCap
- Policy-Weaving Filter via Safety Games
- Policy Weaving as a Safety Game
- Definition of the Policy-Weaving Problem
- From Policy Weaving to Safety Games
- Solving SEVPA Safety Games with Scaffolds
- Definition and Key Properties of Scaffolds
- An Algorithm Parametrized on Scaffolds
- Experiments
- Related Work
- References
- Verification and Synthesis
- Alternate and Learn: Finding Witnesses without Looking All over
- Introduction
- Motivating Examples and Overview
- Alternating Scope Expansion
- Learning Pertinent Scopes
- Preliminaries and Intra-procedural Analysis
- Backward, Forward and Alternating Expansions
- Alternating Expansion
- Learning for Efficient Expansion
- Examples Illustrating the Learning Algorithm
- Evaluation
- Related Work
- Conclusions
- References
- A Complete Method for Symmetry Reduction in Safety Verification
- Introduction
- Related Work
- Preliminaries
- Symmetry
- State Interpolation
- Motivating Examples
- Symmetry Reduction Algorithm
- Experimental Evaluation
- Conclusion
- References
- Synthesizing Number Transformations from Input-Output Examples
- Introduction
- Motivating Examples
- Overview of the Synthesis Approach
- Number Transformations
- Number Transformation Language Ln
- Data Structure for a Set of Expressions in Ln
- Synthesis Algorithm
- Combining Number Transformations with Syntactic String Transformations
- The Combination Language Lc
- Data Structure for Representing a Set of Expressions in Lc
- Synthesis Algorithm
- Experiments
- Related Work
- Conclusions
- References
- Tool Demonstration Papers
- Acacia+, a Tool for LTL Synthesis
- Introduction
- Underlying Approach
- Tool Description
- Application Scenarios
- References
- MGSyn: Automatic Synthesis for Industrial Automation
- Introduction
- Modeling Industrial Automation Processes with Games
- Example: Synthesizing Executable Code for FESTO MPS
- Back-end Engine and Execution Platform Mapping
- Concluding Remarks
- References
- OpenNWA: A Nested-Word Automaton Library
- Introduction
- NWAs
- The OpenNWA library
- Automata-Theoretic Operations
- Client Information
- Inter-operability with WPDSs
- Uses of OpenNWA
- Related work
- References
- Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification
- Introduction
- The Implementation and Architecture of Ufo
- Preprocessing Phase
- Analysis Phase
- Instantiations of Ufo
- Conclusion
- References
- SAFARI: SMT-Based Abstraction for Arrays with Interpolants
- Introduction
- The Tool
- Discussion
- Experiments
- References
- Bma: Visual Tool for Modeling and Analyzing Biological Networks
- Introduction
- Designing Biological Networks
- Analyzing Biological Networks
- Conclusion
- References
- APEX: An Analyzer for Open Probabilistic Programs
- Introduction
- How APEX Works
- Automaton Construction
- Equivalence Checking
- Comparison with Other Tools
- Novel Features
- References
- Recent Developments in FDR
- Introduction
- New Techniques and Features
- Technical Details, Availability and Usage
- References
- A Model Checker for Hierarchical Probabilistic Real-Time Systems
- Introduction
- Modeling with PRTS
- System Analysis
- Simulation
- Verification
- Implementation and Experiments
- Conclusion
- References
- SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs
- Introduction
- SymDiff
- Interface for Source Languages
- C Front End
- Conclusion and Related Work
- References
- Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems
- Tool Overview
- System Description Language
- Implementation Details and Optimizations
- Multi-core Architecture
- Experimental Results and Future Works
- References
- HybridSAL Relational Abstracter
- Introduction
- Relational Abstraction of Linear Systems
- The HybridSal Relational Abstracter
- Related Work and Conclusion
- References
- Euler: A System for Numerical Optimization of Programs
- Introduction
- Using Euler
- System Internals
- Results
- References
- SPT: Storyboard Programming Tool
- Introduction
- Overview: Linked List Deletion
- Algorithm
- Tool Architecture
- Experiments and Tool Experiences
- References
- CSolve: Verifying C with Liquid Types
- Introduction
- Architecture, Use, and Availability
- Example
- References
- passert: A Tool for Debugging Parallel Programs
- Introduction
- The Parallel Assertion Language
- Syntax
- Assertion Semantics
- Applicability of Parallel Assertions to Real World Bugs
- Tool Design
- Response to Assertion Failure
- Timing modes
- Strict Timing
- Relaxed Timing
- Results
- Conclusion
- References
- TRACER: A Symbolic Execution Tool for Verification
- Introduction
- State-Of-The-Art Interpolation-Based Verification Tools
- How tracer Works
- Usage and Implementation
- Experience with Benchmarks
- References
- Joogie: Infeasible Code Detection for Java
- Introduction
- Joogie Overview
- Bytecode Translation
- Infeasible Code Detection
- Experiments
- Conclusion
- References
- HECTOR: An Equivalence Checker for a Higher-Order Fragment of ML
- Introduction
- Theory and Implementation
- Examples and Experiments
- Related Work, Conclusions and Further Directions
- References
- Resource Aware ML
- Introduction
- The Prototype Implementation
- Experiments
- References
- Author Index
