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