Accepted Papers

Accepted Research Papers

Extending Isabelle/HOL’s Code Generator with support for the Go programming languageTerru Stübinger and Lars Hupel
Fast Attack Graph Defense Localization via BisimulationNimrod Busany, Rafi Shalom, Dan Klein and Shahar Maoz
A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural NetworksEric Goubault and Sylvie Putot
Stochastic Games for User JourneysPaul Kobialka, Andrea Pferscher, Gunnar Rye Bergersen, Einar Broch Johnsen and Silvia Lizeth Tapia Tarifa
Staged Specification Logic for Verifying Higher-Order Imperative ProgramsDarius Foo, Yahui Song and Wei-Ngan Chin
State Matching and Multiple References in Adaptive Active Automata LearningLoes Kruger, Sebastian Junges and Jurriaan Rot
Certified Quantization Strategy Synthesis for Neural NetworksYedi Zhang, Guangke Chen, Fu Song, Jun Sun and Jin Song Dong
Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0Laura Titolo, Mariano Moscato, Marco A. Feliu, Paolo Masci and Cesar Munoz
Partially Observable Stochastic Games with Neural Perception MechanismsRui Yan, Gabriel Santos, Gethin Norman, David Parker and Marta Kwiatkowska
Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal LogicBen 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 CommunicationAbhishek Tiwari, Jyoti Prakash, Zhen Dong and Carlo A. Furia
The Opacity of Timed AutomataJie An, Qiang Gao, Lingtai Wang, Naijun Zhan and Ichiro Hasuo
Unifying Weak Memory Verification using PotentialsLara Bargmann, Brijesh Dongol and Heike Wehrheim
Formal Semantics and Analysis of Multitask PLC ST Programs with PreemptionJaeseo Lee and Kyungmin Bae
fm-weck: Containerized Execution of Formal Methods ToolsDirk Beyer and Henrik Wachowitz
Learning Branching-Time Properties in CTL and ATL via Constraint SolvingBenjamin 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 DafnyTabea Bordis and K. Rustan M. Leino
DFAMiner: Mining minimal separating DFAs from labelled samplesDaniele Dell’Erba, Yong Li and Sven Schewe
Accelerated Bounded Model CheckingFlorian Frohn and Jürgen Giesl
Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic SetsHao 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 ProgramsKrishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi and Ðorđe Žikelić
Understanding Synthesized Reactive Systems Through InvariantsRüdiger Ehlers
Accurate Static Data Race Detection for CEmerson Sales, Omar Inverso and Emilio Tuosto
HyGaViz: Visualizing Game-Based Certificates for Hyperproperty VerificationRaven Beutner, Bernd Finkbeiner and Angelina Göbl
Chamelon : a delta-debugger for OCamlMilla Valnet, Nathanaëlle Courant, Guillaume Bury, Pierre Chambart and Vincent Laviron
Automated Static Analysis of Quality of Service Properties of Communicating SystemsCarlos Gustavo Lopez Pombo, Agustín Eloy Martinez Suñé and Emilio Tuosto
Alloy repair hint generation based on historical dataAna 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 AlgorithmsPengbo Yan, Toby Murray, Olga Ohrimenko, Van-Thuan Pham and Robert Sison
B2SAT: A Bare-Metal Reduction of B to SATMichael Leuschel
Introducing SWIRL: An Intermediate Representation Language for Scientific WorkflowsIacopo Colonnelli, Doriana Medic, Alberto Mulone, Viviana Bono, Luca Padovani and Marco Aldinucci
CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test CasesPedro Orvalho, Mikolas Janota and Vasco Manquinho
Bridging Dimensions: Confident Reachability for High-Dimensional ControllersYuang Geng, Jake Brandon Baldauf, Souradeep Dutta, Chao Huang and Ivan Ruchkin
Detecting speculative execution vulnerabilities on weak memory modelsNicholas Coughlin, Kait Lam, Graeme Smith and Kirsten Winter
The nonexistence of unicorns and many-sorted Löwenheim–Skolem theoremsBenjamin Przybocki, Guilherme Toledo, Yoni Zohar and Clark Barrett
PyBDR: Set-boundary based Reachability Analysis Toolkit in PythonJianqiang Ding, Taoran Wu, Zhen Liang and Bai Xue
VeriQR: A Robustness Verification Tool for Quantum Machine Learning ModelsYanling Lin, Ji Guan, Wang Fang, Mingsheng Ying and Zhaofeng Su
Practical Approximate Quantifier Elimination for Non-linear Real ArithmeticS. 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 ArithmeticValentin Promies and Erika Abraham
Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold AutomataTom Baumeister, Paul Eichler, Swen Jacobs, Mouhammad Sakr and Marcus Völp
Reachability Analysis for Multiloop Programs Using Transition Power AbstractionKonstantin Britikov, Martin Blicha, Natasha Sharygina and Grigory Fedyukovich
Efficient Formally Verified Maximal End Component Decomposition for MDPsArnd Hartmanns, Bram Kohlen and Peter Lammich
Proving Functional Program Equivalence via Directed Lemma SynthesisYican Sun, Ruyi Ji, Jian Fang, Xuanlin Jiang, Mingshuai Chen and Yingfei Xiong
Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at LastSung-Shik Jongmans

Accepted Embedded Systems Track Papers

Compositional Verification of Cryptographic Circuits against Fault Injection AttacksHuiyu Tan, Xi Yang, Fu Song, Taolue Chen and Zhilin Wu
Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid SystemsJulius Adelt, Robert Aron Mensing and Paula Herber
Switching Controller Synthesis for Hybrid Systems Against STL FormulasHan Su, Shenghua Feng, Sinong Zhan and Naijun Zhan
On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded DomainsHao Wu, Shenghua Feng, Gan Ting, Jie Wang, Bican Xia and Naijun Zhan
Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical SystemsChangjian 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 LogicZhenya Zhang, Jie An, Paolo Arcaini and Ichiro Hasuo

Accepted Industry Day Papers

UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model CheckingMinghua Wang, Jingling Xue, Lin Huang, Yuan Zi and Tao Wei
Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock TuningJuntao Ji, Yinyou Gu, Yubao Fu and Qingshan Lin
AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE ModelsHanfeng Wang, Zhibin Yang, Yong Zhou, Xilong Wang, Weilin Deng and Wei Li
Code-level Safety Verification for Automated Driving: A Case StudyVladislav 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 DesignDavid 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.