Witnessing Secure Compilation -- BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results -- Fixing Code That Explodes Under Symbolic Evaluation -- The Correctness of a Code Generator for a Functional Language -- Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification -- Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction -- A Systematic Approach to Abstract Interpretation of Program Transformations -- Sharing ghost variables in a collection of abstract domains -- Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation -- Synthesizing Environment Invariants for Modular Hardware Verification -- Systematic Classi cation of Attackers via Bounded Model Checking -- Cheap CTL Compassion in NuSMV -- A Cooperative Parallelization Approach for Property-Directed k-Induction -- Generalized Property-Directed Reachability for Hybrid Systems -- Language Inclusion for Finite Prime Event Structures -- Promptness and Bounded Fairness in Concurrent and Parameterized Systems -- Solving LIA* Using Approximations -- Formalizing and checking Multilevel Consistency -- Practical Abstractions for Automated Veri cation of Shared-Memory Concurrency -- How to Win First-Order Safety Games -- Improving Parity Game Solvers with Justifications.