Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings

Front Matter....Pages -
The Spirit of Ghost Code....Pages 1-16
SMT-Based Model Checking for Recursive Programs....Pages 17-34
Property-Directed Shape Analysis....Pages 35-51
Shape Analysis via Second-Order Bi-Abduction....Pages 52-68
ICE: A Robust Framework for Learning Invariants....Pages 69-87
From Invariant Checking to Invariant Inference Using Randomized Search....Pages 88-105
SMACK: Decoupling Source Language Details from Verifier Implementations....Pages 106-113
Synthesis of Masking Countermeasures against Side Channel Attacks....Pages 114-130
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies....Pages 131-149
String Constraints for Verification....Pages 150-166
A Conference Management System with Verified Document Confidentiality....Pages 167-183
 Vac - Verifier of Administrative Role-Based Access Control Policies....Pages 184-191
From LTL to Deterministic Automata: A Safraless Compositional Approach....Pages 192-208
Symbolic Visibly Pushdown Automata....Pages 209-225
Engineering a Static Verification Tool for GPU Kernels....Pages 226-242
Lazy Annotation Revisited....Pages 243-259
Interpolating Property Directed Reachability....Pages 260-276
Verifying Relative Error Bounds Using Symbolic Simulation....Pages 277-292
Regression Test Selection for Distributed Software Histories....Pages 293-309
GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components....Pages 310-326
Software Verification in the Google App-Engine Cloud....Pages 327-333
The nuXmv Symbolic Model Checker....Pages 334-342
Analyzing and Synthesizing Genomic Logic Functions....Pages 343-357
Finding Instability in Biological Models....Pages 358-372
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells....Pages 373-390
Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions....Pages 391-406
Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections....Pages 407-423
Verifying LTL Properties of Hybrid Systems with K-Liveness ....Pages 424-440
Safraless Synthesis for Epistemic Temporal Specifications....Pages 441-456
Minimizing Running Costs in Consumption Systems....Pages 457-472
CEGAR for Qualitative Analysis of Probabilistic Systems....Pages 473-490
Optimal Guard Synthesis for Memory Safety....Pages 491-507
Don’t Sit on the Fence....Pages 508-524
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications....Pages 525-532
Solving Games without Controllable Predecessor....Pages 533-540
 G4LTL-ST : Automatic Generation of PLC Programs....Pages 541-549
Automatic Atomicity Verification for Clients of Concurrent Data Structures....Pages 550-567
Regression-Free Synthesis for Concurrency....Pages 568-584
Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization....Pages 585-602
An SMT-Based Approach to Coverability Analysis....Pages 603-619
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes....Pages 620-627
Monadic Decomposition....Pages 628-645
A DPLL( T ) Theory Solver for a Theory of Strings and Regular Expressions....Pages 646-662
Bit-Vector Rewriting with Automatic Rule Generation....Pages 663-679
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors....Pages 680-695
AVATAR: The Architecture for First-Order Theorem Provers....Pages 696-710
Automating Separation Logic with Trees and Data....Pages 711-728
A Nonlinear Real Arithmetic Fragment....Pages 729-736
Yices 2.2....Pages 737-744
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis....Pages 745-761
Symbolic Resource Bound Inference for Functional Programs....Pages 762-778
Proving Non-termination Using Max-SMT....Pages 779-796
Termination Analysis by Learning Terminating Programs....Pages 797-813
Causal Termination of Multi-threaded Programs....Pages 814-830
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)....Pages 831-848
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction....Pages 849-865
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers....Pages 866-873
Back Matter....Pages -