Computer Aided Verification

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.