Computer Aided Verification

Invited Talks.- Singularity: Designing Better Software (Invited Talk).- Coping with Outside-the-Box Attacks.- Invited Tutorials.- Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial).- Theorem Proving for Verification (Invited Tutorial).- Tutorial on Separation Logic (Invited Tutorial).- Abstract Interpretation with Applications to Timing Validation.- Session 1: Concurrency.- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis.- Monitoring Atomicity in Concurrent Programs.- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings.- A Hybrid Type System for Lock-Freedom of Mobile Processes.- Session 2: Memory Consistency.- Implied Set Closure and Its Application to Memory Consistency Verification.- Effective Program Verification for Relaxed Memory Models.- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses.- Session 3: Abstraction/Refinement.- Automated Assume-Guarantee Reasoning by Abstraction Refinement.- Local Proofs for Linear-Time Properties of Concurrent Programs.- Probabilistic CEGAR.- Session 4: Hybrid Systems.- Computing Differential Invariants of Hybrid Systems as Fixedpoints.- Constraint-Based Approach for Analysis of Hybrid Systems.- Session 5: Tools – Dynamic Verification.- AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems.- FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement.- Session 6: Modeling and Specification Formalisms.- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems.- Conflict-Tolerant Features.- Ranking Automata and Games for Prioritized Requirements.- Session 7: Decision Procedures.- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations.- Linear Arithmetic with Stars.- Inferring Congruence Equations Using SAT.- Session 8: Tools – Decision Procedures.- The Barcelogic SMT Solver.- The MathSAT 4 SMT Solver.- CSIsat: Interpolation for LA+EUF.- Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B.- Session 9: Program Verification.- Heap Assumptions on Demand.- Proving Conditional Termination.- Monotonic Abstraction for Programs with Dynamic Memory Heaps.- Enhancing Program Verification with Lemmas.- Session 10: Program and Shape Analysis.- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis.- Scalable Shape Analysis for Systems Code.- Thread Quantification for Concurrent Shape Analysis.- Session 11: Tools – Security and Program Analysis.- The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols.- The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis.- Jakstab: A Static Analysis Platform for Binaries.- THOR: A Tool for Reasoning about Shape and Arithmetic.- Session 12: Hardware Verification I.- Functional Verification of Power Gated Designs by Compositional Reasoning.- A Practical Approach to Word Level Model Checking of Industrial Netlists.- Session 13: Hardware Verification II.- Validating High-Level Synthesis.- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths.- Application of Formal Word-Level Analysis to Constrained Random Simulation.- Session 14: Model Checking.- Producing Short Counterexamples Using “Crucial Events”.- Discriminative Model Checking.- Session 15: Space Efficient Algorithms.- Correcting a Space-Efficient Simulation Algorithm.- Semi-external LTL Model Checking.- Session 16: Tools – Model Checking.- QMC: A Model Checker for Quantum Systems.- T(O)RMC: A Tool for (?)-Regular Model Checking.- Faster Than Uppaal?.