Computer Aided Verification
23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings
Published on 5. July 2011
XV, 763 pages
978-3-642-22110-1 (ISBN)
Description
This book constitutes the refereed proceedings of the 23rd International Conference on Computer Aided Verification, CAV 2011, held in Snowbird, UT, USA, in July 2011.
The 35 revised full papers presented together with 20 tool papers were carefully reviewed and selected from 161 submissions. The papers are organized in topical sections on the following workshops: 4th International Workshop on Numerical Software Verification (NSV 2011), 10th International Workshop on Parallel and Distributed Methods in Verifications (PDMC 2011), 4th International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2 2011), Frontiers in Analog Circuit Synthesis and Verification (FAC 2011), International Workshop on Satisfiability Modulo Theories, including SMTCOMP (SMT 2011), 18th International SPIN Workshop on Model Checking of Software (SPIN 2011), Formal Methods for Robotics and Automation (FM-R 2011), and Practical Synthesis for Concurrent Systems (PSY 2011).
More details
Other editions
Additional editions
Ganesh Gopalakrishnan | Shaz Qadeer
Computer Aided Verification
23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings
Book
07/2011
Springer
€53.49
Available immediately
Content
- Title
- Preface
- Organization
- Table of Contents
- HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection
- Introduction
- Paper Organization
- Example: SQL Injection
- The Hampi String Constraint Solver
- Hampi Input Language for String Constraints
- Core Form of String Constraints
- Bit-Vector Encoding and Solving
- Example of Hampi Constraint Solving
- Evaluation
- Identifying SQL Injection Vulnerabilities Using Static Analysis
- Creating SQL Injection Attacks Using Dynamic Analysis
- Systematic Testing of C Programs
- Related Work
- References
- Using Types for Software Verification
- SMT-Based Modular Analysis of Sequential Systems Code
- Introduction
- Basic Memory Model
- Types
- Formalizing Types
- SMT Theory for Types
- Low-Level Data Structures
- Reachability Predicate
- Modeling Low-Level Lists
- Other Challenges
- References
- Logic and Compositional Verification of Hybrid Systems
- Introduction
- Hybrid Systems
- Undecidability of Numerical Image Computation
- Hybrid Programs
- Hybrid Automata
- Logic for Hybrid Systems
- Compositional Deductive Verification
- Verification Tool KeYmaera
- References
- Using Coverage to Deploy Formal Verification in a Simulation World
- Introduction
- ASIC Verification Process
- Coverage Metrics in Simulation
- Measuring Coverage with Formal Verification
- Mutation Coverage
- Conclusion
- References
- Stability in Weak Memory Models
- Context
- Covering Relations
- Synchronisation Idioms
- Locks
- Read-Modify-Write Primitives
- Stability from a Weak Architecture to SC
- offence: A Synchronisation Tool
- Control Flow Graphs and Critical Cycles
- Placing Synchronisation Primitives
- Experiments
- Related Work and Conclusion
- References
- Verification of Certifying Computations
- Introduction
- Outline of Approach
- Tool Overview: VCC and Isabelle/HOL
- Case Study: Maximum Cardinality Matching in Graphs
- Checker
- Formal Proof of Witness Property
- Linking VCC and Isabelle
- Evaluation
- Related Work
- Conclusion and Future Work
- References
- Parameter Identification for Markov Models of Biochemical Reactions
- Introduction
- Discrete-State Stochastic Model
- Dynamic State Space Truncation
- Parameter Inference
- Numerical Approximation Algorithm
- State-Based Likelihood Approximation
- Path-Based Likelihood Approximation
- Experimental Results
- Equidistant Time Series
- Non-equidistant Time Series
- Related Work
- Conclusion
- References
- Getting Rid of Store-Buffers in TSO Analysis
- Introduction
- Concurrent Programs
- Syntax
- SC Semantics
- TSO Semantics
- Reachability Problems
- Bounded-Round Reachability: From TSO to SC
- Simulating Store Buffers: Case k=1
- Simulating Store Buffers: General Case
- Code-to-Code Translation
- Bounded Store-Age Reachability
- Experiments
- Conclusion
- References
- Malware Analysis with Tree Automata Inference
- Introduction
- Related Work
- Notation and Terminology
- k-Testable Tree Automata Inference
- Congruence Relation
- Inference Algorithm
- Experimental Results
- Benchmarks
- Malware and Goodware Recognition
- Malware Classification
- Limitations
- Conclusions and Future Work
- References
- State/Event-Based LTL Model Checking under Parametric Generalized Fairness
- Introduction
- Fairness Expressed in a State/Event-Based Logic
- Parameterized Fairness as Quantified SE-LTL
- Quantification of Parametric SE-LTL Formulas
- Finite Instantiation Property and Parameter Abstraction
- Path-Realized Parameters for an LKS Satisfying FIP
- Automata-Based Model Checking Algorithm
- Automata-Based Characterization
- On-The-Fly Model Checking Algorithm
- Parameterized Fairness Case Studies
- Evolving Dining Philosophers Problem
- Balanced Sliding Window Protocol
- Experimental Results
- Conclusions
- References
- Resolution Proofs and Skolem Functions in QBF Evaluation and Applications
- Introduction
- Preliminaries
- Quantified Boolean Formulae
- Q-Resolution
- Skolemization and Skolem Functions
- QBF Certificates
- Model/Countermodel Construction from Resolution Proofs
- Applications to Boolean Relation Determinization
- Experimental Results
- Conclusions and Future Work
- References
- The BINCOA Framework for Binary Code Analysis
- Introduction
- DBA in a Nutshell
- Modelling Low Level Programs with DBA
- The BINCOA Framework
- Related Work
- Conclusion and Perspectives
- References
- CVC4
- Introduction
- Design of CVC4
- Expressions (``nodes'')
- Theories
- Proofs
- Library API
- Theory Modularity
- Support for Concurrency
- Conclusion
- References
- SLAyer: Memory Safety for Systems-Level Code
- Introduction
- Example
- Applying SLAyer to Device Drivers
- SLAyer Program Analysis
- Prover
- Symbolic Execution and Abstraction
- Experimental Results and Availability
- References
- CPAchecker: A Tool for Configurable Software Verification
- Overview
- Architecture and Implementation
- Experimental Evaluation
- References
- Existential Quantification as Incremental SAT
- Introduction
- Worked Example
- Enumerating Implicants
- Enumerating Shortest Implicants
- Over-Approximation by Dualisation
- Reprise and Reflection
- Formal Correctness
- Experiments
- Benchmarks
- Projecting Using Prime Implicants
- Projecting Using BDDs
- Generalising Implicants
- Related Work
- Consensus Method and Resolution
- Hybrid Methods and McMillan's Method
- Methods Based on Integer Linear Programming
- Methods Based on Primes and Cubes
- Concluding Discussion
- References
- EÆcient Analysis of Probabilistic Programs with an Unbounded Counter
- Introduction
- Definitions
- Expected Termination Time
- Finiteness of The Expected Termination Time
- Efficient Approximation of Finite Expected Termination Time
- Quantitative Model-Checking of -Regular Properties
- Experimental Results, Future Work
- References
- Model Checking Algorithms for CTMDPs
- Introduction
- Basic Definitions
- Continuous Stochastic Logic
- CSL
- Optimal Values and Policies
- Model Checking Algorithm
- Optimal Gain Vector for Rsmax(CItrue)
- Cumulative Reward Rsmax(Ct)
- Probabilistic Operator Psmax( UI)
- Interval Cumulative Reward Rsmax(CI)
- Instantaneous Reward Rsmax(It)
- Computational Approaches
- Case Studies
- Introductory Example
- Work Station Cluster
- Further Empirical Evaluation
- Related Work
- Conclusions
- References
- Quantitative Synthesis for Concurrent Programs
- Introduction
- The Quantitative Synthesis Problem
- Partial Programs
- The Performance Model
- The Partial Program Resolution Problem
- Quantitative Games on Graphs
- Imperfect Information Games for Partial Program Resolution
- Complexity of ImpIn Games and Partial-Program Resolution
- Practical Solutions for Partial-Program Resolution
- Experiments
- Conclusion
- References
- Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with B¨uchi Objectives
- Introduction
- Definitions
- Symbolic Algorithms for B¨uchi Objectives
- A New Subquadratic Algorithm
- Symbolic Implementation of IMPRALGO
- The Win-Lose Algorithm
- The Basic Win-Lose Algorithm
- Improved WINLOSE Algorithm and Symbolic Implementation
- Improved Symbolic SCC Algorithm
- Experimental Results
- References
- Smoothing a Program Soundly and Robustly
- Introduction
- Smooth Interpretation
- Approximate Smooth Interpreters and their Correctness
- Designing a Smooth Interpreter
- Properties of the Interpreter
- Related Work and Conclusion
- References
- A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification
- Introduction
- Motivating Example
- Formal Preliminaries
- A Specialization Calculus
- Inferring Specializable Predicates
- Experiments
- Related Work and Conclusion
- References
- KRATOS - A Software Model Checker for SystemC
- Introduction
- Verification Flow
- Architecture
- Novel Functionalities
- Conclusion and Future Work
- References
- Efficient Scenario Verification for Hybrid Automata
- Introduction
- Networks of Hybrid Automata
- Networks of Transition Systems
- Hybrid Automata
- SMT Encoding of Hybrid Automata
- Message Sequence Charts
- MSCs for Networks of Hybrid Automata
- Standard Global Automata Construction
- Exploiting Independent Events
- Scenario-Driven Encoding
- Encoding Tailored to MSCs
- Incrementality
- Scenario-Driven Invariants Generation
- Related Work
- Experimental Evaluation
- Conclusions
- References
- Temporal Property Verification as a Program Analysis Task
- Introduction
- From Temporal Logic to Program Analysis
- Preliminaries
- Encoding
- Looking for M
- Correctness
- Example
- Related work
- Experiments
- Conclusions
- References
- Time for Statistical Model Checking of Real-Time Systems
- Context
- The Toolset
- Case Studies
- Firewire Protocol
- Bluetooth Protocol
- Conclusion
- References
- Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs
- Introduction
- Predicate Abstraction Using Mixed Predicates
- Symmetry-Aware Predicate Abstraction
- Mixed Predicates and Notify-All Updates
- Implementing Notify-All Updates
- The Predicate Abstraction Algorithm
- Symmetry-Aware Predicate Abstraction with Aliasing
- Aliasing, Locations of Expressions, and Targets of L-Values
- Shared, Local and Mixed Predicates in the Presence of Aliasing
- Closing the CEGAR Loop
- Experimental Results
- Related Work and Conclusion
- References
- Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic
- Introduction
- Lists Used in The Linux Kernel
- A Note on the Implementation of Predator
- Experiments with Predator
- Conclusion
- References
- SpaceEx: Scalable Verification of Hybrid Systems
- Introduction
- Reachability of Hybrid Systems
- Hybrid Automata
- High-Level Reachability Algorithm
- Support Functions and Template Polyhedra
- Variable Time-Step Flowpipe Computation
- Approximation Model
- Time Step Adaptation with Error Bounds
- Computing Transition Successors
- Experimental Results
- Filtered Oscillator Benchmark
- Helicopter Controller
- Conclusions
- References
- From Cardiac Cells to Genetic Regulatory Networks
- Introduction
- Biological Switching
- The Minimal Resistor Model
- The Minimal Conductance Model
- The Piecewise-Multiaffine Model
- Cardiac Disorder Parameter-Range Identification
- Conclusions and Future Work
- References
- Threader: A Constraint-Based Verifier for Multi-threaded Programs
- Introduction
- Threader Overview
- Experiments
- References
- Interactive Synthesis of Code Snippets
- Introduction
- Examples
- Foundations and Algorithm
- InSynth Implementation and Evaluation
- References
- Forest Automata for Verification of Heap Manipulation
- Introduction
- From Heaps to Forests
- Hypergraphs and Their Representation
- Hypergraphs
- A Forest Representation of Hypergraphs
- Minimal and Canonical Forests
- Forest Automata
- Hierarchical Hypergraphs
- Hierarchical Hypergraphs, Components, and Boxes
- Hierarchical Forest Automata
- Inclusion and Well-Connectedness on Hierarchical SFA
- The Verification Procedure Based on Forest Automata
- Implementation and Experimental Results
- Conclusion
- References
- Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints
- Introduction
- Models and Constraints
- Static Cyclic Scheduling
- ILP Modulo Theories
- Formal Preliminaries
- Lazy IMT Approach
- Theory Lemmas
- Unschedulable Cores
- Subsumption
- Lemma Generation
- Memoization
- Resource Limits
- Related Work
- Experimental Evaluation
- Conclusions and Future Work
- References
- µZ- An Efficient Engine for Fixed Points with Constraints
- Introduction
- Architecture
- Rule Transformations
- Compilation to an Abstract Machine
- Execution
- Tables and Relations
- Usage
- Conclusion
- References
- BAP: A Binary Analysis Platform
- Introduction
- BAP Goals and Related Work
- BAP Architectural Overview
- BAP Capabilities
- Analyses and Optimizations.
- Verification Conditions.
- Applications
- Limitations
- Conclusion
- References
- HMC: Verifying Functional Programs Using Abstract Interpreters
- Introduction
- Overview
- Step 1: Constraint Generation
- Step 2: Translation to Imperative Program
- Experiments
- Discussions: Completeness
- References
- A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations
- Introduction
- Quantifier Elimination for a Conjunction of LMCs
- Dropping Unconstraining LMDs
- Splitting and Model Enumeration
- Boolean Combinations of LMCs
- DD Based Approach
- DAG Based Approach
- Experimental Results
- Conclusion
- References
- Bug-Assist: Assisting Fault Localization in ANSI-C Programs
- Introduction
- Tool Description
- User Guide
- The Integrated Debugging Environment
- Tool Architecture
- References
- Synthesis of Distributed Control through Knowledge Accumulation
- Introduction
- Preliminaries
- A Globally Controlled System
- Knowledge Based Distributed Control
- Control Using Knowledge Accumulating Supervisors
- Implementing Supervisors
- Experimental Results
- Conclusions
- References
- Language Equivalence for Probabilistic Automata
- Introduction
- Algorithms for Equivalence Checking
- Deterministic Algorithms
- Randomised Algorithms
- Runtime
- Extracting Counterexamples
- Experiments
- Herman's Protocol
- Grade Protocol
- Randomised Inflation
- Conclusion
- References
- Formalization and Automated Verification of RESTful Behavior
- Introduction
- REST and its Formalization
- Building Blocks for Rest
- Formalizing Resource-Based Applications
- Formalization of RESTful Behavior
- Rest on Http, and Variations
- Formal RESTful HTTP
- Variations on RESTful HTTP Properties
- Distinguishing REST from HTTP
- Automated Verification of RESTful Behavior
- Computation Model
- Fundamental Questions
- Automata Constructions
- Model-Checking for Fixed Instances
- Parameterized Verification
- Run-Time Monitoring
- Synthesizing Servers
- Relaxing the Atomicity of Communications
- Related Work and Conclusions
- References
- Linear Completeness Thresholds for Bounded Model Checking
- Introduction
- Definitions
- Büchi Automata with Linear Completeness Thresholds
- Cliquey Büchi Automata
- Computing Completeness Thresholds of Cliquey Automata
- Linear Temporal Logic and Cliquey Automata
- Beyond Cliqueyness
- Linear Completeness Thresholds without Cliqueyness
- Büchi Automata with Non-linear Completeness Thresholds
- Concluding Remarks
- References
- Interpolation-Based Software Verification with Wolverine
- Introduction
- Implementation
- Interface for Interpolating Decision Procedures
- Checking Linux Device Drivers
- Conclusion
- References
- Synthesizing Biological Theories
- Introduction
- Main Challenges and Design Principles
- The SBT Language and Tool
- Classes, Objects, Types
- Generalized Charts
- Subcharts
- Symbolic Instances
- Execution Modes
- Deterministic vs. Nondeterministic Execution
- Stepping Mode
- Configurations
- Display Options
- Biological Examples and Future Directions
- References
- PRISM 4.0: Verification of Probabilistic Real-Time Systems
- Introduction
- Functionality Overview
- Probabilistic Timed Automata (PTAs)
- Other New PRISM Components and Features
- References
- Program Analysis for Overlaid Data Structures
- Introduction
- Informal Description
- Formal Setting for Region Variables
- Abstract States
- Pre-analysis
- Invariant Inference
- Experiments
- Conclusion
- References
- KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs
- Introduction
- Extended Executor for C++ Programs
- Optimizations
- Experimental Results
- References
- Fully Symbolic Model Checking for Timed Automata
- Introduction
- Preliminaries - Timed Automata
- Finite State Machines with Time
- Model Checking Algorithm
- From Timed Automata to FSMTs
- First Steps of Translation
- Modifications for Pure Interleaving Behavior
- Modifications for Parallelized Interleaving Behavior
- Computation of a Symbolic Representation
- Experimental Results
- Conclusions
- References
- Complete Formal Hardware Verification of Interfaces for a FlexRay-Like Bus
- Introduction
- Models for Hardware with Multiple Clock Domains
- The Detailed Model
- The Hybrid Model and the Bus
- Transmitting Bits across the Bus
- Modeling the Bus
- An Alternative Model
- Related Work and Results Used
- Overall Proof
- Global Assumptions
- Proof Sketch of the Bus Value Correctness
- Message Transmission Correctness
- Conclusion and Future Work
- References
- Synthia: Verification and Synthesis for Timed Automata
- Introduction
- Underlying Approach
- The Tool Synthia
- Experimental Results
- References
- FixBag : A Fixpoint Calculator for Quantified Bag Constraints
- Introduction
- Motivating Examples
- Algorithm
- Experimental Results
- Related Works and Conclusion
- References
- Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoP
- Introduction
- Technical Overview
- Unsynthesizable Specifications and Undesirable Behavior
- Analyzing a Specification in LTLMoP
- Conclusions and Future Work
- References
- Practical, Low-Effort Equivalence Verification of Real Code
- Introduction
- Overview
- Handling Uninteresting Mismatches
- Implementation
- Referents: Tracking Which Memory Contains Pointers
- Object Comparison
- Lazy Initialization
- Limitations
- Evaluation
- Different Implementations: Newlib vs. uClibc
- Different Versions of the Same Implementation: uClibc
- Checking the Checker: Finding Bugs in UC-KLEE and LLVM
- Results summary
- Related Work
- Conclusion
- References
- Relational Abstractions for Continuous and Hybrid Systems
- Introduction
- Preliminaries
- Relational Abstractions
- Relational Abstractions of Hybrid Systems
- Implementation
- Experimental Evaluation
- Conclusions
- References
- Simplifying Loop Invariant Generation Using Splitter Predicates
- Introduction
- An Overview of the Technique
- Language
- Splitter Predicates
- Algorithm for Splitting
- Revisiting the Running Example
- Implementation
- Experiments
- Related Work
- Conclusion
- References
- Monitorability of Stochastic Dynamical Systems
- Introduction
- Related Work
- Definitions and Notation
- Conditions for Monitorability
- Strong Monitorability
- Monitorability
- Monitoring Algorithms
- Example
- Conclusion
- References
- Equality-Based Translation Validator for LLVM
- Introduction
- Overview
- Implementation
- Results
- References
- Model Checking Recursive Programs with Numeric Data Types
- Introduction
- Preliminaries
- Pushdown Systems with Counters and Clocks
- Upper Bounds for Model Checking PCo
- Lower Bounds for Model Checking PCo
- Adding clocks
- Experimental Results
- Extensions and Future Work
- References
- Author Index
