E-raamat: 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

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 Girls 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.- Dont 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 Simpleand 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.