Tools for Ensuring Software Correctness
Preface...................................................................................................................................VII Chapter 1 Formal Reasoning About the Security of Amazon Web Services................................. 1 Byron Cook Chapter 2 Propositional Dynamic Logic for Higher-Order Functional Programs.................................................................................................................................10 Yuki Satake and Hiroshi Unno Chapter 3 Exploiting Synchrony and Symmetry in Relational Verification................................ 28 Lauren Pick, Grigory Fedyukovich and Aarti Gupta Chapter 4 Eager Abstraction for Symbolic Model Checking.......................................................... 47 Kenneth L. McMillan Chapter 5 Counterexample Guided Inductive Synthesis Modulo Theories............................... 65 Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening and Elizabeth Polgreen Chapter 6 Constraint-Based Synthesis of Coupling Proofs............................................................ 83 Aws Albarghouthi and Justin Hsu Chapter 7 Synthesis of Asynchronous Reactive Programs from Temporal Specifications....................................................................................................................... 102 Suguman Bansal, Kedar S. Namjoshi and Yaniv Sa’ar Chapter 8 Learning Abstractions for Program Synthesis.............................................................. 121 Xinyu Wang, Greg Anderson, Isil Dillig and K. L. McMillan Chapter 9 Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes.................................................................................................... 141 Hui Kong, Ezio Bartocci and Thomas A. Henzinger Chapter 10 Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems.................................................................................................................... 160 Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz and Ji?í Srba Chapter 11 Strix: Explicit Reactive Synthesis Strikes Back!............................................................ 179 Philipp J. Meyer, Salomon Sickert and Michael Luttenberger Chapter 12 Nagini: A Static Verifier for Python................................................................................ 187 Marco Eilers and Peter Müller Chapter 13 Sound Value Iteration........................................................................................................ 195 Tim Quatmann and Joost-Pieter Katoen Chapter 14 Semantic Adversarial Deep Learning............................................................................. 213 Tommaso Dreossi, Somesh Jha and Sanjit A. Seshia Permissions List of Contributors Index Contents