Neural Network Robustness as a Verification Property: a Principled Case Study

Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir and Idan Refaeli

Sound Automation of Magic Wands

Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller and Alexander J. Summers

SMT-Based Translation Validation for Machine Learning Compiler

Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo and Juneyoung Lee

Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation

Andreas Gittis, Eric Vin and Daniel Fremont

Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition

Yong Li, Andrea Turrini, Weizhi Feng, Moshe Vardi and Lijun Zhang

End-to-End Mechanised Proof of an eBPF Virtual Machine for Microcontrollers

Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg and Emmanuel Baccelli

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures

Lorenz Leutgeb, Georg Moser and Florian Zuleger

Murxla: a Modular and Highly Extensible API Fuzzer for SMT Solvers

Aina Niemetz, Mathias Preiner and Clark Barrett

Complementing Büchi Automata with Ranker

Vojtěch Havlena, Ondrej Lengal and Barbora Šmahlíková

Affine Loop Invariant Generation via Matrix Algebra

Yucheng Ji, Hongfei Fu, Bin Fang and Haibo Chen

UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis

Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora and Sanjit A. Seshia

Sampling-Based Verification of CTMCs with Uncertain Rates

Thom Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga and Matthias Volk

Playing Against Fair Adversaries in Stochastic Games with Total Rewards

Pablo Castro, Pedro R. D'Argenio, Ramiro Demasi and Luciano Putruele

STLmc: Robust STL Model Checking of Hybrid Systems Using SMT

Geunyeol Yu, Jia Lee and Kyungmin Bae

From Spot 2.0 to Spot 2.10: What's New?

Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard and Henrich Lauko

RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems

Eric Goubault and Sylvie Putot

Verifying Fairness in Quantum Machine Learning

Ji Guan, Wang Fang and Mingsheng Ying

Hemiola: a DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols

Joonwon Choi, Adam Chlipala and Arvind

Example Guided Synthesis of Linear Approximations for Neural Network Verification

Brandon Paulsen and Chao Wang

Reasoning About Data Trees Using CHCs

Marco Faella and Gennaro Parlato

PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation

Yuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang and Wanwei Liu

Shared Certificates for Neural Network Verification

Marc Fischer, Christian Sprecher, Dimitar I. Dimitrov, Gagandeep Singh and Martin Vechev

Trainify: a CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning

Peng Jin, Jiaxu Tian, Dapeng Zhi, Xuejun Wen and Min Zhang