| Title | Authors |
| Extending Isabelle/HOL’s Code Generator with support for the Go programming language | Terru Stübinger and Lars Hupel |
| Fast Attack Graph Defense Localization via Bisimulation | Nimrod Busany, Rafi Shalom, Dan Klein and Shahar Maoz |
| A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks | Eric Goubault and Sylvie Putot |
| Stochastic Games for User Journeys | Paul Kobialka, Andrea Pferscher, Gunnar Rye Bergersen, Einar Broch Johnsen and Silvia Lizeth Tapia Tarifa |
| Staged Specification Logic for Verifying Higher-Order Imperative Programs | Darius Foo, Yahui Song and Wei-Ngan Chin |
| State Matching and Multiple References in Adaptive Active Automata Learning | Loes Kruger, Sebastian Junges and Jurriaan Rot |
| Certified Quantization Strategy Synthesis for Neural Networks | Yedi Zhang, Guangke Chen, Fu Song, Jun Sun and Jin Song Dong |
| Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0 | Laura Titolo, Mariano Moscato, Marco A. Feliu, Paolo Masci and Cesar Munoz |
| Partially Observable Stochastic Games with Neural Perception Mechanisms | Rui Yan, Gabriel Santos, Gethin Norman, David Parker and Marta Kwiatkowska |
| Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic | Ben Greenman, Siddhartha Prasad, Shufang Zhu, Giuseppe De Giacomo, Shriram Krishnamurthi, Marco Montali, Tim Nelson, Milda Zizyte and Antonio Di Stasio |
| Automated Repair of Information Flow Security in Android Implicit Inter-App Communication | Abhishek Tiwari, Jyoti Prakash, Zhen Dong and Carlo A. Furia |
| The Opacity of Timed Automata | Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan and Ichiro Hasuo |
| Unifying Weak Memory Verification using Potentials | Lara Bargmann, Brijesh Dongol and Heike Wehrheim |
| Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption | Jaeseo Lee and Kyungmin Bae |
| fm-weck: Containerized Execution of Formal Methods Tools | Dirk Beyer and Henrik Wachowitz |
| Learning Branching-Time Properties in CTL and ATL via Constraint Solving | Benjamin Bordais, Daniel Neider and Rajarshi Roy |
| A Local Search Algorithm for MaxSMT(LIA) | Xiang He, Bohan Li, Mengyu Zhao and Shaowei Cai |
| Free Facts: An Alternative to Inefficient Axioms in Dafny | Tabea Bordis and K. Rustan M. Leino |
| DFAMiner: Mining minimal separating DFAs from labelled samples | Daniele Dell’Erba, Yong Li and Sven Schewe |
| Accelerated Bounded Model Checking | Florian Frohn and Jürgen Giesl |
| Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets | Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan and Gan Ting |
| Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs | Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi and Ðorđe Žikelić |
| Understanding Synthesized Reactive Systems Through Invariants | Rüdiger Ehlers |
| Accurate Static Data Race Detection for C | Emerson Sales, Omar Inverso and Emilio Tuosto |
| HyGaViz: Visualizing Game-Based Certificates for Hyperproperty Verification | Raven Beutner, Bernd Finkbeiner and Angelina Göbl |
| Chamelon : a delta-debugger for OCaml | Milla Valnet, Nathanaëlle Courant, Guillaume Bury, Pierre Chambart and Vincent Laviron |
| Automated Static Analysis of Quality of Service Properties of Communicating Systems | Carlos Gustavo Lopez Pombo, Agustín Eloy Martinez Suñé and Emilio Tuosto |
| Alloy repair hint generation based on historical data | Ana Inês Barros, Henrique Neto, Alcino Cunha, Nuno Macedo and Ana C. R. Paiva |
| Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms | Pengbo Yan, Toby Murray, Olga Ohrimenko, Van-Thuan Pham and Robert Sison |
| B2SAT: A Bare-Metal Reduction of B to SAT | Michael Leuschel |
| Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows | Iacopo Colonnelli, Doriana Medic, Alberto Mulone, Viviana Bono, Luca Padovani and Marco Aldinucci |
| CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases | Pedro Orvalho, Mikolas Janota and Vasco Manquinho |
| Bridging Dimensions: Confident Reachability for High-Dimensional Controllers | Yuang Geng, Jake Brandon Baldauf, Souradeep Dutta, Chao Huang and Ivan Ruchkin |
| Detecting speculative execution vulnerabilities on weak memory models | Nicholas Coughlin, Kait Lam, Graeme Smith and Kirsten Winter |
| The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems | Benjamin Przybocki, Guilherme Toledo, Yoni Zohar and Clark Barrett |
| PyBDR: Set-boundary based Reachability Analysis Toolkit in Python | Jianqiang Ding, Taoran Wu, Zhen Liang and Bai Xue |
| VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models | Yanling Lin, Ji Guan, Wang Fang, Mingsheng Ying and Zhaofeng Su |
| Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic | S. Akshay, Supratik Chakraborty, Amir Kafshdar Goharshady, R. Govind, Harshit Jitendra Motwani and Sai Teja Varanasi |
| A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic | Valentin Promies and Erika Abraham |
| Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata | Tom Baumeister, Paul Eichler, Swen Jacobs, Mouhammad Sakr and Marcus Völp |
| Reachability Analysis for Multiloop Programs Using Transition Power Abstraction | Konstantin Britikov, Martin Blicha, Natasha Sharygina and Grigory Fedyukovich |
| Efficient Formally Verified Maximal End Component Decomposition for MDPs | Arnd Hartmanns, Bram Kohlen and Peter Lammich |
| Proving Functional Program Equivalence via Directed Lemma Synthesis | Yican Sun, Ruyi Ji, Jian Fang, Xuanlin Jiang, Mingshuai Chen and Yingfei Xiong |
| Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at Last | Sung-Shik Jongmans |
