Computer Aided Verification

Invited Talks.- Policy Monitoring in First-Order Temporal Logic.- Retrofitting Legacy Code for Security.- Quantitative Information Flow: From Theory to Practice?.- Memory Management in Concurrent Algorithms.- Invited Tutorials.- ABC: An Academic Industrial-Strength Verification Tool.- There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code.- Constraint Solving for Program Verification: Theory and Practice by Example.- Session 1. Software Model Checking.- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data.- Termination Analysis with Compositional Transition Invariants.- Lazy Annotation for Program Testing and Verification.- The Static Driver Verifier Research Platform.- Dsolve: Safety Verification via Liquid Types.- Contessa: Concurrency Testing Augmented with Symbolic Analysis.- Session 2. Model Checking and Automata.- Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing.- Efficient Emptiness Check for Timed Büchi Automata.- Session 3. Tools.- Merit: An Interpolating Model-Checker.- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems.- Jtlv: A Framework for Developing Verification Algorithms.- Petruchio: From Dynamic Networks to Nets.- Session 4. Counter and Hybrid Systems Verification.- Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems.- Safety Verification for Probabilistic Hybrid Systems.- A Logical Product Approach to Zonotope Intersection.- Fast Acceleration of Ultimately Periodic Relations.- An Abstraction-Refinement Approach to Verification of Artificial Neural Networks.- Session 5. Memory Consistency.- Fences in Weak Memory Models.- Generating Litmus Tests for Contrasting Memory Consistency Models.- Session 6. Verification of Hardware and Low Level Code.- Directed Proof Generation for Machine Code.- Verifying Low-Level Implementations of High-Level Datatypes.- Automatic Generation of Inductive Invariants from