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