Relational Differential Dynamic Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
Juraj Kolčák, Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata,
David Sprunger, and Akihisa Yamada
Verifying Concurrent Systems
Assume, Guarantee or Repair . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211
Hadar Frenkel, Orna Grumberg, Corina Pasareanu,
and Sarai Sheinvald
Structural Invariants for the Verification of Systems
with Parameterized Architectures. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228
Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis,
and Christoph Welzel
Automated Verification of Parallel Nested DFS. . . . . . . . . . . . . . . . . . . . . . 247
Wytse Oortwijn, Marieke Huisman, Sebastiaan J. C. Joosten,
and Jaco van de Pol
Discourje: Runtime Verification of Communication Protocols in Clojure . . . . 266
Ruben Hamers and Sung-Shik Jongmans
Probabilistic Systems
Scenario-Based Verification of Uncertain MDPs . . . . . . . . . . . . . . . . . . . . . 287
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen,
and Ufuk Topcu
Good-for-MDPs Automata for Probabilistic Analysis
and Reinforcement Learning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 306
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi,
Ashutosh Trivedi, and Dominik Wojtczak
Farkas Certificates and Minimal Witnesses for Probabilistic
Reachability Constraints. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 324
Florian Funke, Simon Jantsch, and Christel Baier
Simple Strategies in Multi-Objective MDPs . . . . . . . . . . . . . . . . . . . . . . . . 346
Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann,
and Mickael Randour
Model Checking and Reachability
Partial Order Reduction for Deep Bug Finding in Synchronous Hardware . . . 367
Makai Mann and Clark Barrett
xviii
Contents – Part I