- Accepted Research Papers
- Accepted Embedded Systems Track Papers
- Accepted Industry Day Papers
- Accepted Tutorial Papers
Accepted Research Papers
| 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 |
Accepted Embedded Systems Track Papers
| Title | Authors |
| Compositional Verification of Cryptographic Circuits against Fault Injection Attacks | Huiyu Tan, Xi Yang, Fu Song, Taolue Chen and Zhilin Wu |
| Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems | Julius Adelt, Robert Aron Mensing and Paula Herber |
| Switching Controller Synthesis for Hybrid Systems Against STL Formulas | Han Su, Shenghua Feng, Sinong Zhan and Naijun Zhan |
| On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains | Hao Wu, Shenghua Feng, Gan Ting, Jie Wang, Bican Xia and Naijun Zhan |
| Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems | Changjian Zhang, Parv Kapoor, Romulo Meira-Goes, David Garlan, Eunsuk Kang, Akila Ganlath, Shatadal Mishra and Nejib Ammar |
| CauMon: An Informative Online Monitor for Signal Temporal Logic | Zhenya Zhang, Jie An, Paolo Arcaini and Ichiro Hasuo |
Accepted Industry Day Papers
| Title | Authors |
| UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking | Minghua Wang, Jingling Xue, Lin Huang, Yuan Zi and Tao Wei |
| Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning | Juntao Ji, Yinyou Gu, Yubao Fu and Qingshan Lin |
| AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models | Hanfeng Wang, Zhibin Yang, Yong Zhou, Xilong Wang, Weilin Deng and Wei Li |
| Code-level Safety Verification for Automated Driving: A Case Study | Vladislav Nenchev, Calum Imrie, Simos Gerasimou and Radu Calinescu |
| Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT) | Bjarne Johansson, Marjan Sirjani, Edward Lee, Zahra Moezkarimi, Bahman Pourvatan, Stefan Marksteiner and Alessandro Papadopoulos |
| A Case Study on Formal Equivalence Verification between a C/C++ Model and its RTL Design | David Vincenzoni, Gaetano Raia, Gianluca Rigano and Maurizio Martina |
Accepted Tutorial Papers
Monday, September 9th, morning:
- The Pyramid Of (Formal) Software Verification (Martin Brain, Elizabeth Polgreen): Over the past few years, there has been significant progress in the various fields of software verification resulting in many useful tools and successful deployments, both academic and commercial. However much of the work describing these tools and ideas is written by and for the research community. The scale, diversity, and focus of the existing literature can act as a barrier, separating industrial users and the wider academic community from the tools that could make their work more efficient, more certain, and more productive. This paper gives a simple classification of verification techniques in terms of a pyramid and uses it to describe the six main schools of verification technologies. We have found this approach valuable and successful for building collaborations with industry as it allows us to explain the intrinsic strengths and weaknesses of various techniques and pick the right tool for any given industrial application. The model also highlights some of the cultural differences and unspoken assumptions of various areas of verification and illuminates future directions.
- No risk, no fun: a tutorial on risk management (Marielle Stoelinga): The aim of this tutorial is twofold: first, it explains the area of risk management and its most prominent concepts: the definition of risk, strategies for managing risk, the risk management cycle, and several related concepts. Second, it provides a (necessarily incomplete) overview of several prominent approaches in formal methods geared toward better risk management. These methods help to make risk management more accountable: systematic, transparent, and quantitative.
- Advancing Quantum Computing with Formal Methods (Arend-Jan Quist, Jingyi Mei, Tim Coopmans, Alfons Laarman): This tutorial provides an introduction to quantum computing with a focus on the applicability of formal methods on it. We will describe quantum circuits and convey an intuitive understanding of their inherent combinatorial nature and the resulting exponential blow-up that makes them hard to analyze. Then, we show how two automated reasoning techniques, weighted model counting and decision diagrams, can be used to solve hard analysis tasks for quantum circuits. This tutorial is aimed at everyone in the formal methods community with an interest in quantum computing. Familiarity with quantum computing is not required, but basic linear algebra knowledge (particularly: what is a basis of a vector space and how does a matrix act on it by matrix-vector multiplication?) and elementary complex number arithmetic are a prerequisite. The goal of the tutorial is to get the formal methods community inspired to use automated reasoning techniques to advance the development of quantum computing.
Monday, September 9th, afternoon:
- Copilot Tutorial (Ivan Perez, Alwyn Goodloe, Frank Dedden): Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enables monitoring these systems in runtime, to detect property violations early and limit their potential consequences. This paper is a tutorial on RV using Copilot, a runtime verification framework for real-time embedded systems. Copilot monitors are written in a compositional, stream-based language with support for a variety of Temporal Logics (TL), which results in robust, high-level specifications that are easier to understand than their traditional counterparts. The framework translates monitor specifications into C code with static memory requirements, which can be compiled to run on embedded hardware.
- ASMETA tool set for rigorous system design (Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene and Patrizia Scandurra): This tutorial paper introduces ASMETA, a comprehensive suite of integrated tools around the Abstract State Machine formal method to specify and analyze the executable behavior of discrete event systems. ASMETA supports the entire system development life-cycle, from the specification of the functional requirements to the implementation of the code, in a systematic way. This tutorial provides an overview of ASMETA through an illustrative case study, the Pill-Box, related to the design of a smart pillbox device. It illustrates the practical use of the range of modeling and V&V techniques and C++ code generation from models available in ASMETA to increase the quality and reliability of behavioral system models and source code.
- Practical Deductive Verification of OCaml Programs (Mário Pereira): Functional languages have evolved from academic artifacts into mature and flexible environments on which one can develop efficient, real-world software. With languages of such family gaining momentum within industry, one might natural pose the question on how to apply formal methods to ensure the correctness of software written in a functional language. In this paper, we chose the OCaml language as our working vehicle and provide a comprehensive, hands-on tutorial on how to apply deductive verification to OCaml-written programs. In particular, we show how one can use the GOSPEL specification language and the Cameleer tool to conduct mostly-automated verification on OCaml code. In our presentation, we focus on two main classes of programs: first, purely functional programs with no mutable state; then on imperative programs, where one can mix mutable state with subtle control-flow primitives, such as locally-defined exceptions.
Tuesday, September 10th, morning:
- Software Verification with CPAchecker: Tutorial and User Guide (Daniel Baier, Dirk Beyer, Po-Chun Chien, Marie-Christine Jakobs, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch-Rosenfeld, Henrik Wachowitz, Philipp Wendler): This tutorial provides an introduction to CPAchecker, which is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as predicates, constant values, intervals, BDDs, and memory graphs, and many program-analysis and model-checking algorithms, such as symbolic execution, predicate abstraction, bounded model checking, k-induction, PDR, interpolation-based model checking, and IMPACT. The software system originates from Simon Fraser University, Universität Passau, and Ludwig-Maximilians-Universität München and received many contributions from other institutions, such as Universität Paderborn, Universität Oldenburg, Technische Universität Darmstadt, and ISP\,RAS. The development history spans 17 years and more than 120 developers worldwide have contributed to its success. This tutorial presents basic use cases for CPAchecker in formal software verification, explains the main verification techniques of CPAchecker with their strengths and weaknesses, and how to use CPAchecker for test-case generation and verification-result validation.
- Satisfiability Modulo Theories: A Beginner’s Tutorial (Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar): Great minds have long dreamed of creating machines that can reason deductively and automatically and can thereby function as general-purpose problem solvers. Satisfiability modulo theories (SMT) has emerged as one pragmatic realization of this dream, providing significant expressive power without giving up automation. This tutorial is a beginner’s guide to the capabilities and uses of modern SMT solvers. It includes a basic overview of SMT and its formal foundations, a catalog of the main theories used in SMT solvers, and illustrations of how to use SMT solvers to obtain models and proofs. Throughout the tutorial, many examples and exercises are provided. These are designed to be hands-on activities for the reader. They can be run using either Python or the SMT-LIB language, using either the cvc5 or the Z3 SMT solvers.
Tuesday, September 10th, afternoon:
- A Tutorial on Stream-based Monitoring (Jan Baumeister, Bernd Finkbeiner, Florian Kohn, Frederik Scheerer): Stream-based runtime monitoring frameworks are safety assurance tools that check the runtime behavior of a system against a formal specification. This tutorial provides a hands-on introduction to RTLola, a real-time monitoring toolkit for cyber-physical systems and networks. RTLola processes, evaluates, and aggregates streams of input data, such as sensor readings, and provides a real-time analysis in the form of comprehensive statistics and logical assessments of the system’s health. RTLola has been applied successfully in the monitoring of autonomous systems such as unmanned aircraft. The tutorial guides the reader through the development of a stream-based specification for an autonomous drone observing other flying objects in its flight path. Each section of the tutorial provides both an intuitive introduction for RTLola novices, highlighting useful language features and specification patterns, and a more in-depth explanation of technical details for the advanced reader. Finally, we discuss how runtime monitors generated from RTLola specifications can be integrated into a variety of systems.
- The Java Verification Tool KeY: A Tutorial (Bernhard Beckert, Richard Bubel, Daniel Drodt, Reiner Hähnle, Florian Lanzinger, Wolfram Pfeifer, Mattias Ulbrich and Alexander Weigl): The KeY tool is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable, because one can prove one method at a time to be correct relative to its contract. KeY combines auto-active and fine-grained proof interaction, which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date. The article provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods.