Accepted Papers

Lorenz Leutgeb, Georg Moser and Florian ZulegerAutomated Expected Amortised Cost Analysis of Probabilistic Data Structures
Marco Faella and Gennaro ParlatoReasoning about Data Trees using CHCs
Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo and Juneyoung LeeSMT-based Translation Validation for Machine Learning Compiler
Ji Guan, Wang Fang and Mingsheng YingVerifying Fairness in Quantum Machine Learning
Long H. Pham and Jun SunVerifying Neural Networks Against Backdoor Attacks
Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir and Idan RefaeliNeural Network Robustness as a Verification Property: A Principled Case Study
Joonwon Choi, Adam Chlipala and ArvindHemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols
Eric Goubault and Sylvie PutotRINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems
Yuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang and Wanwei LiuPoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation
Shaowei Cai, Bohan Li and Xindi ZhangLocal Search For SMT on Linear Integer Arithmetic
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 LaukoFrom Spot 2.0 to Spot 2.10: What’s New?
Thom Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga and Matthias VolkSampling-Based Verification of CTMCs with Uncertain Rates
Vojtěch Havlena, Ondrej Lengal and Barbora ŠmahlíkováComplementing Büchi Automata with Ranker
Peng Jin, Jiaxu Tian, Dapeng Zhi, Xuejun Wen and Min ZhangTrainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani and Rajeev AlurSpecification-Guided Learning of Nash Equilibria with High Social Welfare
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer and Đorđe ŽikelićSound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga and Kohei SuenagaOblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Yong Li, Andrea Turrini, Weizhi Feng, Moshe Vardi and Lijun ZhangDivide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition
Yucheng Ji, Hongfei Fu, Bin Fang and Haibo ChenAffine Loop Invariant Generation via Matrix Algebra
Priyanka Golia, Brendan Juba and Kuldeep S. MeelA Scalable Shannon Entropy Estimator
Kyveli Doveri, Pierre Ganty and Nicolas MazzocchiFORQ-based Language Inclusion Formal Testing
Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias WinklerDoes a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
Leonardo Alt, Martin Blicha, Antti Hyvärinen and Natasha SharyginaSolCMC: Solidity Compiler’s Model Checker
Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez and Albert RubioDistilling Constraints in Zero-Knowledge Protocols
Joshua M. Cohen, Qinshi Wang and Andrew W. AppelVerified Erasure Correction in Coq with MathComp and VST
Anna Becchi and Alessandro CimattiAbstraction Modulo Stability for Reverse Engineering
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora and Sanjit A. SeshiaUCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Aina Niemetz, Mathias Preiner and Clark BarrettMurxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers
Michael Blondin, Filip Mazowiecki and Philip OfftermattVerifying generalised and structural soundness of workflow nets via relaxations
Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg and Emmanuel BaccelliEnd-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
Pablo Castro, Pedro R. D’Argenio, Luciano Putruele and Ramiro DemasiPlaying Against Fair Adversaries in Stochastic Games with Total Rewards
Jingbo Wang, Yannan Li and Chao WangSynthesizing Fair Decision Trees via Iterative Constraint Solving
Raven Beutner and Bernd FinkbeinerSoftware Verification of Hyperproperties Beyond k-SafetyDistinguished Paper Award
Andreas Gittis, Eric Vin and Daniel FremontRandomized Synthesis for Diversity and Cost Constraints with Control Improvisation
Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett and Cesare TinelliEven Faster Conflicts and Lazier Reductions for String Solvers
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller and Alexander J. SummersSound Automation of Magic Wands
Sebastian Junges and Matthijs T. J. SpaanAbstraction-Refinement for Hierarchical Probabilistic Models
Brandon Paulsen and Chao WangExample Guided Synthesis of Linear Approximations for Neural Network Verification
Stanley Bak, Sergiy Bogomolov, Brandon Hencey, Niklas Kochdumper, Ethan Lew and Kostiantyn PotomkinReachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
Andreas Katis, Anastasia Mavridou, Dimitra Giannakopoulou, Thomas Pressburger and Johann SchumannCapture, Analyze, Diagnose: Realizability Checking of Requirements in FRET
Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu and Subhajit RoyData-Driven Invariant Learning for Probabilistic ProgramsDistinguished Paper Award
Prantik Chatterjee, Jaydeepsinh Meda, Akash Lal and Subhajit RoyProof-guided Underapproximation Widening for Bounded Model Checking
Chaitanya Agarwal, Shibashis Guha, Jan Křetínský and Pazhamalai MuruganandhamPAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga and Ichiro HasuoThe Lattice-Theoretic Essence of Property Directed Reachability Analysis
Ahmed Bouajjani, Wael-Amine Boutglay and Peter HabermehlData-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger and Julian SiberExplaining Hyperproperty Violations
Marc Fischer, Christian Sprecher, Dimitar I. Dimitrov, Gagandeep Singh and Martin VechevShared Certificates for Neural Network Verification
Timo P. Gros, Holger Hermanns, Joerg Hoffmann, Michaela Klauck, Maximilian Alexander Köhl and Verena WolfMoGym: Using Formal Models for Training and Verifying Decision-making Agents
Bernd Finkbeiner, Niklas Metzger and Yoram MosesInformation Flow Guided Synthesis
Mateus De Oliveira OliveiraSynthesis and Analysis of Petri Nets from Causal Specifications
Geunyeol Yu, Jia Lee and Kyungmin BaeSTLmc: Robust STL Model Checking of Hybrid Systems using SMT