Computer Aided Verification

This book constitutes the proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 46 regular papers and 11 short papers presented in this volume were carefully reviewed and selected from a total of 175 regular and 54 short paper submissions. The contributions are organized in topical sections named: software verification; automata; model checking and testing; biology and hybrid systems; games and synthesis; concurrency; SMT and theorem proving; bounds and termination; and abstraction.

Inhalt

Software Verification.- The Spirit of Ghost Code.- SMT-Based Model Checking for Recursive Programs.- Property-Directed Shape Analysis.- Shape Analysis via Second-Order Bi-Abduction.- ICE: A Robust Framework for Learning Invariants.- From Invariant Checking to Invariant Inference Using Randomized Search.- SMACK: Decoupling Source Language Details from Verifier Implementations.- Security.- Synthesis of Masking Countermeasures against Side Channel Attacks.- Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.- String Constraints for Verification.- A Conference Management System with Verified Document Confidentiality.- VAC - Verifier of Administrative Role-Based Access Control Policies.- Automata.- From LTL to Deterministic Automata: A Safraless Compositional Approach.- Symbolic Visibly Pushdown Automata.- Model Checking and Testing.- Engineering a Static Verification Tool for GPU Kernels.- Lazy Annotation Revisited.- Interpolating Property Directed Reachability.- Verifying Relative Error Bounds Using Symbolic Simulation.- Regression Test Selection for Distributed Software Histories.- GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components.- Software Verification in the Google App-Engine Cloud.- The nuXmv Symbolic Model Checker.- Biology and Hybrid Systems Analyzing and Synthesizing Genomic Logic Functions.- Finding Instability in Biological Models.- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells.- Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions.- Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections.- Verifying LTL Properties of Hybrid Systems with K-Liveness.- Games and Synthesis.- Safraless Synthesis for Epistemic Temporal Specifications.- Minimizing Running Costs in Consumption Systems.- CEGAR for Qualitative Analysis of Probabilistic Systems.- Optimal Guard Synthesis for Memory Safety.- Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion.- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications.- Solving Games without Controllable Predecessor.- G4LTL-ST: Automatic Generation of PLC Programs.- Concurrency.- Automatic Atomicity Verification for Clients of Concurrent Data Structures.- Regression-Free Synthesis for Concurrency.- Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization.- An SMT-Based Approach to Coverability Analysis.- LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes.- SMT and Theorem Proving.- Monadic Decomposition.- A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.- Bit-Vector Rewriting with Automatic Rule Generation.- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors.- AVATAR: The Architecture for First-Order Theorem Provers.- Automating Separation Logic with Trees and Data.- A Nonlinear Real Arithmetic Fragment.- Yices 2.2.- Bounds and Termination.- A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis.- Symbolic Resource Bound Inference for Functional Programs.- Proving Non-termination Using Max-SMT.- Termination Analysis by Learning Terminating Programs.- Causal Termination of Multi-threaded Programs.- Abstraction.- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR).- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction.- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers.