| Tobias John, Simon Jantsch, Christel Baier and Sascha Klüppelholz. |
Determinization and Limit-determinization of Emerson-Lei automata (Best Paper Award) |
| Bernd Finkbeiner, Felix Klein, and Niklas Metzger. |
Live Synthesis |
| Vedad Hadžić, Robert Primas and Roderick Bloem. |
Proving SIFA Protection of Masked Redundant Circuits |
| Brae Webb, Mark Utting and Ian Hayes. |
A Formal Semantics of the GraalVM Intermediate Representation |
| Zixin Huang, Saikat Dutta and Sasa Misailovic. |
Aqua: Automated Quantized Inference for Probabilistic Programs |
| Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao and Arie Gurfinkel. |
Verifying Verified Code |
| Orna Kupferman, Nir Lavee and Salomon Sickert. |
Certifying DFA Bounds for Recognition and Separation |
| Christel Baier, Florian Funke, Simon Jantsch, Jakob Piribauer and Robin Ziemek. |
Probabilistic causes in Markov Chains |
| Alessandro Cimatti, Alberto Griggio and Enrico Magnago. |
Automatic discovery of fair paths in infinite-state transition systems |
| Jean-Raphaël Gaglione, Daniel Neider, Rajarshi Roy, Ufuk Topcu and Zhe Xu. |
Learning Linear Temporal Properties from Noisy Data: A MaxSAT-based Approach |
| Bernd Finkbeiner and Noemi Passing. |
Compositional Synthesis of Modular Systems |
| Peter Gjøl Jensen, Stefan Schmid, Morten Konggaard Schou, Jiri Srba, Juan Vanerio and Ingo van Duijn. |
Faster Pushdown Reachability Analysis with Applications in Network Verification |
| Shaun Azzopardi, Nir Piterman and Gerardo Schneider. |
Incorporating Monitors in Reactive Synthesis without Paying the Price |
| Lukas Stevens and Tobias Nipkow. |
A Verified Decision Procedure for Orders in Isabelle/HOL |
| Murad Akhundov, Federico Mora, Nick Feng, Vincent Hui and Marsha Chechik. |
Verification by Gambling on Program Slices |
| Igor Khmelnitsky, Daniel Neider, Rajarshi Roy, Xuan Xie, Benoît Barbot, Benedikt Bollig, Alain Finkel, Serge Haddad, Martin Leucker and Lina Ye. |
Property-Directed Verification and Robustness Certification of Recurrent Neural Networks |
| Guillaume Dupont, Yamine Ait Ameur, Marc Pantel and Neeraj Singh. |
Event-B Refinement for Continuous Behaviours Approximation |
| Norine Coenen, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann and Yannick Schillo. |
Runtime Enforcement of Hyperproperties |
| Sara Mohammadinejad, Jyotirmoy V. Deshmukh and Laura Nenzi. |
Mining Interpretable Spatio-temporal Logic Properties for Spatially Distributed Systems |
