Rong Gu, Cristina Seceleanu, Eduard Enoiu and Kristina Lundqvist. Model Checking Collision Avoidance of Nonlinear Autonomous Vehicle Models

Oyendrila Dobe, Erika Abraham, Ezio Bartocci and Borzoo Bonakdarpour. HyperProb: A Model Checker for Probabilistic Hyperproperties

Bing Sun, Jun Sun, Ting Dai and Lijun Zhang. Probabilistic Verification of Neural Networks Against Group Fairness

Gal Amram, Shahar Maoz, Or Pistiner and Jan Oliver Ringert. Efficient Algorithms for ω-Regular Energy Games

Alexei Kopylov, Stefan Mitsch, Aleksey Nogin and Michael Warren. Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers

Matt Griffin and Brijesh Dongol. Verifying Secure Speculation in Isabelle/HOL

Felix A. Wolf, Malte Schwerhoff and Peter Müller. Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA

Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao and Ichiro Hasuo. Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study

Rim Saddem-Yagoubi, Pascal Poizat and Sara Houhou. Business Processes Meet Spatial Concerns: the sBPMN Verification Framework

Mark Batty, Brijesh Dongol and Daniel Wright. Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies

Julius Adelt, Timm Liebrenz and Paula Herber. Formal Verification of Intelligent Hybrid Systems that are modeled with Simulink and the Reinforcement Learning Toolbox

Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen and Laura Kovács. The Probabilistic Termination Tool Amber

Adel Djoudi, Martin Hana and Nikolai Kosmatov. Formal verification of a JavaCard virtual machine with Frama-C

Felipe Gorostiaga and Cesar Sanchez. HStriver: a Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams

Matias Scharager, Katherine Cordwell, Stefan Mitsch and André Platzer. Verified Quadratic Virtual Substitution for Real Arithmetic

Nicholas Coughlin, Kirsten Winter and Graeme Smith. Rely/guarantee reasoning for multicopy atomic weak memory models

Franck Cassez. Verification of the Incremental Merkle Tree Algorithm with Dafny

Weijiang Hong, Zhenbang Chen, Yide Du and Ji Wang. Trace Abstraction-based Verification for Uninterpreted Programs

Cui Su and Jun Pang. CABEAN 2.0: Efficient and Efficacious Control of Asynchronous Boolean Networks

Jinting Bian, Hans-Dieter Hiep, Frank De Boer and Stijn De Gouw. Integrating ADTs in KeY and their Application to History-based Reasoning

Yong Li, Yih-Kuen Tsay, Andrea Turrini, Moshe Vardi and Lijun Zhang. Congruence Relations for Büchi Automata

Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky and Djordje Zikelic. On Lexicographic Proof Rules for Probabilistic Termination

František Blahoudek, Murat Cubuktepe, Petr Novotný, Melkior Ornik, Pranay Thangeda and Ufuk Topcu. Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption

Ionut Tutu, Claudia Chirita and José Luiz Fiadeiro. Dynamic Reconfiguration via Typed Modalities

Simon Foster, Mario Gleirscher, Jonathan Huerta Y Munive and Georg Struth. Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs

Andrea Pferscher and Bernhard K. Aichernig. Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning

Alexandra Bugariu, Arshavir Ter-Gabrielyan and Peter Müller. Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers

Maurice ter Beek, Guillermina Cledou, Rolf Hennicker and José Proença. Featured Team Automata

Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak. Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives

Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka and Vijay Ganesh. Z3str4: A Multi-armed String Solver

Anastasia Mavridou, Andreas Katis, Dimitra Giannakopoulou, David Kooi, Thomas Pressburger and Michael W. Whalen. From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET

Joseph Scott, Hammad Rehman, Trishal Sudula, Federico Mora and Vijay Ganesh. BanditFuzz: Fuzzing SMT Solvers with Multi-Agent Reinforcement Learning

Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin and Philippa Gardner. Two mechanisations of WebAssembly 1.0

Krishna S, Khushraj Madnani, Manuel Mazo Jr. and Paritosh Pandya. Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers

Zhenya Zhang and Paolo Arcaini. Gaussian Process-Based Confidence Estimation for Hybrid System Falsification