Contents – Part I
Program Verification
Software Verification with PDR: An Implementation of the State
of the Art. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
Dirk Beyer and Matthias Dangl
Verifying Array Manipulating Programs with Full-Program Induction . . . . . .
22
Supratik Chakraborty, Ashutosh Gupta, and Divyesh Unadkat
Interpretation-Based Violation Witness Validation for C: NITWIT . . . . . . . .
40
Jan Švejda, Philipp Berger, and Joost-Pieter Katoen
A Calculus for Modular Loop Acceleration . . . . . . . . . . . . . . . . . . . . . . . .
58
Florian Frohn
SAT and SMT
Mind the Gap: Bit-vector Interpolation recast over Linear
Integer Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
79
Takamasa Okudono and Andy King
Automated and Sound Synthesis of Lyapunov Functions
with SMT Solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
97
Daniele Ahmed, Andrea Peruffo, and Alessandro Abate
A Study of Symmetry Breaking Predicates and Model Counting . . . . . . . . . . 115
Wenxi Wang, Muhammad Usman, Alyas Almaawi, Kaiyuan Wang,
Kuldeep S. Meel, and Sarfraz Khurshid
MUST: Minimal Unsatisfiable Subsets Enumeration Tool . . . . . . . . . . . . . . 135
Jaroslav Bendík and Ivana Černá
Timed and Dynamical Systems
Safe Decomposition of Startup Requirements: Verification and Synthesis . . . . 155
Alessandro Cimatti, Luca Geatti, Alberto Griggio, Greg Kimberly,
and Stefano Tonetta
Multi-agent Safety Verification Using Symmetry Transformations . . . . . . . . . 173
Hussein Sibai, Navid Mokhlesi, Chuchu Fan, and Sayan Mitra