Programme

Programme of main conferences from Monday to Thursday. Best Paper candidates are highlighted in yellow and by asterisk.

Monday 08 April

08:45
Opening
10:00
Coffee break
TACAS: SAT and SMT
Room:
10:30
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike and John Backes
11:00
Z3-Noodler: An Automata-based String Solver*
Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč
11:15
TaSSAT: Transferring and Sharing in SAT
Md Solimul Chowdhury, Cayden Codel and Marijn Heule
11:30
Speculative SAT modulo SAT
Hari Govind Vediramana Krishnan, Isabel Garcia-Contreras, Sharon Shoham and Arie Gurfinkel
12:00
Happy ending: An empty hexagon in every set of 30 points
Marijn Heule and Manfred Scheucher
TACAS: Synthesis
Room:
10:30
Fully Generalized Reactivity(1) Synthesis
Rüdiger Ehlers and Ayrat Khalimov
11:00
Knor: reactive synthesis using Oink
Tom van Dijk, Feije van Abbema and Naum Tomov
11:30
On Dependent Variables in Reactive Synthesis
S. Akshay, Eliyahu Basa, Dror Fried and Supratik Chakraborty
12:00
CESAR: Control Envelope Synthesis via Angelic Refinements
Aditi Kabra, Jonathan Laurent, Stefan Mitsch and André Platzer
FASE: Runtime Approaches
Room:
10:30
Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models
Lucas Sakizloglou, Holger Giese, and Leen Lambers
11:00
Probabilistic Runtime Enforcement of Executable BPMN Processes
Yliès Falcone, Gwen Salaün, and Ahang Zuo
11:30
Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems*
He Xu, Sven Schneider, and Holger Giese
12:00
Formal Specification of Trusted Execution Environment APIs
Geunyeol Yu, Seunghyun Chae, Kyungmin Bae, and Sungkun Moon
Rust
Chair:
Room:
10:30
12:30
Lunch
TACAS: Proof Checking
Room:
14:00
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
Hanna Lachnitt, Cesare Tinelli, Andrew Reynolds, Andres Noetzli, Haniel Barbosa, Leni Aniva, Clark Barrett and Mathias Fleury
14:30
Automate where Automation Fails: Proof Strategies for Frama-C/WP
Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov
14:45
VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification
Mertcan Temel
15:00
A State-of-the-Art Karp-Miller Algorithm Certified in Coq
Thibault Hilaire, David Ilcinkas and Jérôme Leroux
15:30
A Logical Treatment of Finite Automata
Nishant Rodrigues, Mircea Sebe, Xiaohong Chen and Grigore Rosu
FASE: System Comprehension
Room:
14:00
Monitoring the Future of Smart Contracts
Margarita Capretto, Martin Ceresa, and Cesar Sanchez
14:30
Comprehending Object State via Dynamic Class Invariant Learning
Jan H. Boockmann, and Gerald Luettgen
15:00
Smart Issue Detection for Large-Scale Online Service Systems Using Multi-Channel Data*
Liushan Chen, Yu Pei, Mingyang Wan, Zhihui Fei, Tao Liang, and Guojun Ma
15:30
Refinement Verification of OS Services based on a Verified Preemptive Microkernel
Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang, and Zhiping Shi
Rust
Chair:
Room:
14:00
SV-COMP
Chair: Dirk Beyer
Room:
14:00
Diversity & Inclusion
Chair:
Room:
14:00
16:00
Coffee break
TACAS: Logic and Decidability
Room:
16:30
Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains
Lukas Westhofen, Christian Neurohr, Daniel Neider and Jean Christoph Jung
17:00
Deciding Boolean Separation Logic via Small Models
Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar and Florian Zuleger
17:30
Asynchronous Subtyping by Trace Relaxation
Laura Bocchi, Andy King and Maurizio Murgia
Invited Tutorial
Chair: Lenore Zuck
Room:
Rust
Chair:
Room:
16:30
SV-COMP
Chair: Dirk Beyer
Room:
16:30
Open SV-COMP Community Meeting

Tuesday 09 April

10:00
Coffee Break
FASE: System Comprehension
Room:
10:30
Fuzzy quantitative attack tree analysis
Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg, and Mariëlle Stoelinga
11:00
Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation
Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura, Vasco Manquinho, and Ruben Martins
11:30
Invariant-based Program Repair
Omar Al-Bataineh
11:45
Can ChatGPT support software verification?
Cedric Richter and Heike Wehrheim
12:00
Combining Deductive Verification with Shape Analysis
Téo Bernier, Yani Ziani, Nikolai Kosmatov, and Frédéric Loulergue
12:15
First Steps towards Deductive Verification of LLVM IR
Dré van Oorschot, Marieke Huisman, and Ömer Şakar
TACAS: Program Analysis and Proofs
Room:
10:30
SootUp: A Redesign of the Soot Static Analysis Framework
Kadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo and Dongjie He
11:00
Formally verified asymptotic consensus in robust networks
Mohit Tekriwal, Avi-Tachna Fram, Jean-Baptiste Jeannin, Manos Kapritsos and Dimitra Panagou
11:30
Formally Verifying an Efficient Sorter
Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler and Sascha Witt
12:00
Explainable Online Monitoring of Metric First-Order Temporal Logic
Leonardo Lima, Jonathan Huerta Y Munive and Dmitriy Traytel
FOSSACS: Infinite games
Room:
10:30
Fair Omega-regular Games
Daniel Hausmann, Nir Piterman, Irmak Saglam and Anne-Kathrin Schmuck
11:00
Stochastic Window Mean-payoff Games
Laurent Doyen, Pranshu Gaba and Shibashis Guha
11:30
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
Daniel Hausmann, Mathieu Lehaut and Nir Piterman
12:00
Parity Games on Temporal Graphs
Pete Austin, Sougata Bose and Patrick Totzke
Industry Day
Chair:
Room:
10:30
Invited talk: Formal Verification of Avionics Software
David Delmas (Airbus Operations SAS)
11:00
Collision-Free Trajectories in Automated Driving: Extending a Formal Argumentation From Single Scenarios to Scenario Ranges
Franziska Henze (CARIAD SE)
11:20
[11:20] How Bosch Brings Formal Methods to Autonomous Systems Engineering
Michaela Klauck (Robert Bosch GmbH), Christian Heinzemann and Ralph Lange
11:40
[11:40] Invited talk: European R&D Projects: Participation and Opportunities
Leonardo Tonetto (Advisor ‑ European R&D and Innovation Support)
12:15
[12:15] Networking Session
Each participant can present a 1-minute no-slide pitch about their interests in collaboration
Rust
Chair:
Room:
10:30
12:30
Lunch
TACAS: Model Checking
Chair: Kristin Rozier
Room:
14:00
JPF: From 2003 to 2023
Cyrille Valentin Artho, Pavel Parizek, Daohan Qu, Varadraj Galgali and Pu Yi
14:30
Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking
Muhammad Osama and Anton Wijs
15:00
Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
Lukas Koenig, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Kueperkoch, Dennis Fassbender and Michael Hanselmann
15:30
Enhancing GenMC's Usability and Performance
Michalis Kokologiannakis, Viktor Vafeiadis and Rupak Majumdar
ESOP: Effects and Modal Types
Room:
14:00
Scoped Effects as Parameterized Algebraic Theories
Sam Lindley, Cristina Matache, Sean Moss, Sam Staton, Nicolas Wu and Zhixuan Yang
14:30
Monadic Intersection Types, Relationally*
Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni
15:00
Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis
Jason Z. S. Hu and Brigitte Pientka
15:30
Program Synthesis from Graded Types
Jack Hughes and Dominic Orchard
FOSSACS: Categorical semantics
Room:
14:00
Drawing from an Urn is Isometric
Bart Jacobs
14:30
Enriching Diagrams with Algebraic Operations
Alejandro Villoria, Henning Basold and Alfons Laarman
15:00
Monoidal Extended Stone Duality
Fabian Birkmann, Stefan Milius and Henning Urbat
15:30
Towards a Compositional Framework for Convex Analysis (with Applications to Probability Theory)
Dario Stein and Richard Samuelson
Industry Day
Chair:
Room:
14:00
Invited talk: Next Generation Model-based Testing for Industrial Applications
Jan Peleska (Verified Systems International)
14:30
Invited talk: What Programmers Want from Proof with SPARK
Yannick Moy (AdaCore)
15:00
Retrospective on Formal Verification of a JavaCard Virtual Machine with Frama-C
Adel Djoudi (Thales Digital Identity & Security)
15:20
[15:20] Formal Methods in the Railways: Trajectory and Trends
Thierry Lecomte (Clearsy), Sébastien Agostini, David Déharbe, Julien Molinéro-Pérez, Erwan Mottin and Denis Sabatier
15:40
[15:40] Recommended Practice on Assurance of AI-enabled systems
Odd Ivar Haugen (DNV)
Rust
Chair:
Room:
14:00
Ask-me-anything
Room:
14:00
On Ethics, AI and Programming with Tamar Sharon and Wolfgang Ahrendt
Host: Tom van Dijk
15:00
Putting Science on the Political Agenda with Ana Cavalcanti and Gerald Lüttgen
Host: Sebastian Junges
16:00
Coffee break
TACAS: Automata and Learning
Chair: Anne-Kathrin Schmuck
Room:
16:30
Scalable Tree-based Register Automata Learning*
Paul Fiterau-Brostean, Simon Dierl, Falk Howar, Bengt Jonsson, Konstantinos Sagonas and Fredrik Tåquist
17:00
Small Test Suites for Active Automata Learning
Loes Kruger, Sebastian Junges and Jurriaan Rot
17:30
Mata: A Fast and Simple Finite Automata Library
David Chocholatý, Tomas Fiedor, Vojtěch Havlena, Lukáš Holík, Martin Hruska, Ondrej Lengal and Juraj Síč
Invited Tutorial
Chair: Marieke Huisman
Room:
Industry Day
Chair:
Room:
16:30
Invited talk: From Theory to Practice: What is a contract, really?
Fritz Henglein (Deon Digital)
17:00
Formal Methods in Web3: Success Stories and Opportunities
Franck Cassez (Mantle Research)
17:20
[17:20] Securing the Aptos Framework through formal verification with the Move Prover
Wolfgang Grieskamp (Aptos Labs), Junkil Park and Teng Zhang
17:40
[17:40] Experience Report: Formally Verifying Critical Blockchain Network Component
Bhargav Bhatt (Web3 Foundation)
Rust
Chair:
Room:
16:30

Wednesday 10 April

10:00
Coffee Break
TACAS: Software Verification
Room:
10:30
Accelerated Bounded Model Checking Using Interpolation Based Summaries
Mayank Solanki, Prantik Chatterjee, Akash Lal and Subhajit Roy
11:00
Weakest Precondition Inference for Non-Deterministic Linear Array Programs
Sumanth Prabhu, Deepak D'Souza, Supratik Chakraborty, Venkatesh R and Grigory Fedyukovich
11:30
Automated Software Verification of Hyperliveness
Raven Beutner
12:00
A Comprehensive Specification and Verification of the L4 Microkernel API
Leping Zhang, Yongwang Zhao and Jianxin Li
ESOP: Domain-Specific Languages
Room:
10:30
Circuit Width Estimation via Effect Typing and Linear Dependency
Andrea Colledan and Ugo Dal Lago
11:00
Reconciling Partial and Local Invertibility
Anders Ågren Thuné, Kazutaka Matsuda and Meng Wang
11:30
On the Hardness of Analyzing Quantum Programs Quantitatively
Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix
12:00
Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping
Hiroya Fujinami and Ichiro Hasuo
FOSSACS: Automata and synthesis
Room:
10:30
Determinization of Integral Discounted-Sum Automata is Decidable
Shaull Almagor and Neta Dafni
11:00
Checking History-Determinism is NP-hard for Parity Automata
Aditya Prakash
11:30
Tighter Construction of Tight Büchi Automata
Marek Jankola and Jan Strejček
12:00
Synthesis with Privacy Against an Observer
Orna Kupferman, Ofer Leshkowitz and Naama Shamash Halevy
Spin
Chair:
Room:
10:30
12:30
Lunch
13:00
ETAPS General Assembly
TACAS: Probabilistic Systems
Room:
14:00
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains*
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler
14:30
CTMCs with Imprecisely Timed Observations
Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga and Nils Jansen
15:00
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot and Sebastian Junges
15:30
Learning Explainable and Better Performing Representations of POMDP Strategies
Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky and Stefanie Mohr
ESOP: Bidirectional typing / Session types
Room:
14:00
A formal treatment of bidirectional typing
Liang-Ting Chen and Hsiang-Shang Ko
14:30
Generic bidirectional typing for dependent type theories
Thiago Felicissimo
15:00
The Session Abstract Machine
Luis Caires and Bernardo Toninho
15:30
Deciding Subtyping for Asynchronous Multiparty Sessions
Elaine Li, Felix Stutz and Thomas Wies
FOSSACS: Types and programming languages
Room:
14:00
From Rewrite Rules to Axioms in the lambdaPi-Calculus Modulo Theory
Valentin Blot, Gilles Dowek, Thomas Traversié and Théo Winterhalter
14:30
Light Genericity
Beniamino Accattoli and Adrienne Lancelot
15:00
Logical Predicates in Higher-Order Mathematical Operational Semantics
Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas and Henning Urbat
15:30
On Basic Feasible Functionals and the Interpretation Method
Patrick Baillot, Ugo Dal Lago, Cynthia Kop and Deivid Vale
Spin
Chair:
Room:
14:00
Tool demo session
Chair:
Room:
14:00
16:00
Coffee break
TACAS: Simulations
Room:
16:30
Dissipative quadratizations of polynomial ODE systems
Yubo Cai and Gleb Pogudin
17:00
Forward and Backward Constrained Bisimulations for Quantum Circuits
Antonio Jiménez-Pastor, Kim Guldstrand Larsen, Mirco Tribastone and Max Tschaikowski
17:30
A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation
Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán and Yon Shin Teo
ESOP: Dependent Types
Room:
16:30
Observational Equality Meets CIC
Loïc Pujet and Nicolas Tabareau
17:00
Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance and Assia Mahboubi
17:30
Definitional Functoriality for Dependent (Sub)Types
Théo Laurent, Meven Lennon-Bertrand and Kenji Maillard
TACAS: Neural Networks
Room:
16:30
Provable Preimage Under-Approximation for Neural Networks
Xiyue Zhang, Benjie Wang and Marta Kwiatkowska
17:00
Training for Verification: Increasing Neuron Stability to Scale DNN Verification
Dong Xu, Nusrat Jahan Mozumder, Hai Duong and Matthew Dwyer
17:30
NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis
Matthias Cosler, Christopher Hahn, Ayham Omar and Frederik Schmitt
Spin
Chair:
Room:
16:30

Thursday 11 April

09:00
10:00
Coffee Break
TACAS: Testing and Verification
Room:
10:30
HaliVer: Deductive Verification and Scheduling Languages Join Forces
Lars B. van den Haak, Anton Wijs, Marieke Huisman and Mark van den Brand
11:00
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage
Martin Jonáš, Jan Strejček, Marek Trtík and Lukáš Urban
11:30
Fast Symbolic Computation of Bottom SCCs
Anna Blume Jakobsen, Rasmus Skibdahl Melanchton Jorgensen, Andreas Pavlogiannis and Jaco van de Pol
12:00
Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers
Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee and Nils Sirrenberg
ESOP: Verification and Analysis
Room:
10:30
Verified Inlining and Specialisation for PureCake*
Hrutvik Kanabar, Kacper Korban and Magnus O. Myreen
11:00
Maximal Quantified Precondition Synthesis for Linear Array Loops
Sumanth Prabhu, Grigory Fedyukovich and Deepak D'Souza
11:30
Higher-Order LCTRSs and Their Termination
Liye Guo and Cynthia Kop
12:00
Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
Daniel Lundén, Lars Hummelgren, Jan Kudlicka, Oscar Eriksson and David Broman
FOSSACS: Logic and proofs
Room:
10:30
Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems
Luca Geatti, Alessio Mansutti and Angelo Montanari
11:00
A Resolution-Based Interactive Proof System for UNSAT
Philipp Czerner, Javier Esparza and Valentin Krasotin
11:30
Craig Interpolation for Decidable First-Order Fragments*
Balder ten Cate and Jesse Comer
12:00
Clones, closed categories, and combinatory logic
Philip Saville
Spin
Chair:
Room:
10:30
12:30
Lunch
TACAS: Games
Room:
14:00
Auction-Based Scheduling
Guy Avni, Kaushik Mallik and Suman Sadhukhan
14:30
Most General Winning Secure Equilibria Synthesis in Graph Games
Satya Prakash Nayak and Anne-Kathrin Schmuck
15:00
On-The-Fly Algorithm for Reachability in Parametric Timed Games
Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci and Jaco van de Pol
15:30
Rabin Games and Colourful Universal Trees
Rupak Majumdar, Irmak Saglam and K. S. Thejaswini
ESOP: Verification
Room:
14:00
A Denotational Approach to Release-Acquire Concurrency
Yotam Dvir, Ohad Kammar and Ori Lahav
14:30
Specifying and Verifying Persistent Libraries
Léo Stefanesco, Azalea Raad and Viktor Vafeiadis
15:00
Intel PMDK Transactions: Specification and Concurrency
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer and Brijesh Dongol
15:30
Hyperproperty Verification as CHC Satisfiability
Shachar Itzhaky, Sharon Shoham and Yakir Vizel
FOSSACS: Infinite-state systems
Room:
14:00
Reachability in Fixed VASS: Expressiveness and Lower Bounds
Andrei Draghici, Christoph Haase and Andrew Ryzhikov
14:30
From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
Jan-Christoph Kassing, Florian Frohn and Jürgen Giesl
15:00
Dimension-Minimality and Primality of Counter Nets
Shaull Almagor, Guy Avni, Henry Sinclair-Banks and Asaf Yeshurun
15:30
Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
Lucie Guillou, Corto Mascle and Nicolas Waldburger
Spin
Chair:
Room:
14:00
Test-Comp
Chair: Dirk Beyer
Room:
14:00
Award winner presentations
Chair:
Room:
14:00
16:00
Coffee break
TACAS: Concurrency
Room:
16:30
Verification under TSO with an infinite Data Domain
Florian Furbach, Parosh Aziz Abdulla, Mohamed Faouzi Atig and Shashwat Garg
17:00
OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust*
Nils Husung, Clemens Dubslaff, Holger Hermanns and Maximilian Alexander Köhl
17:30
Decidable Verification under Localized Release-Acquire Concurrency
Abhishek Kr Singh and Ori Lahav
ESOP: Abstract Interpretation
Room:
16:30
A Modular Soundness Theory for the Blackboard Analysis Architecture
Sven Keidel, Dominik Helm, Tobias Roth and Mira Mezini
17:00
Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law*
Raphaël Monat, Aymeric Fromherz and Denis Merigoux
17:30
Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation*
Pierre Lermusiaux and Benoit Montagu
Spin
Chair:
Room:
16:30
Test-Comp
Chair: Dirk Beyer
Room:
16:30
Open Test-Comp Community Meeting
Programme in PDF for print

Accepted Papers

ESOP
  • Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer and Brijesh Dongol. Intel PMDK Transactions: Specification and Concurrency
  • Léo Stefanesco, Azalea Raad and Viktor Vafeiadis. Specifying and Verifying Persistent Libraries
  • Sumanth Prabhu, Grigory Fedyukovich and Deepak D’Souza. Maximal Quantified Precondition Synthesis for Linear Array Loops
  • Hrutvik Kanabar, Kacper Korban and Magnus O. Myreen. Verified Inlining and Specialisation for PureCake
  • Liye Guo and Cynthia Kop. Higher-Order LCTRSs and Their Termination
  • Liang-Ting Chen and Hsiang-Shang Ko. A Formal Treatment of Bidirectional Typing
  • Jack Hughes and Dominic Orchard. Program Synthesis from Graded Types
  • Jason Z. S. Hu and Brigitte Pientka. Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis
  • Sven Keidel, Dominik Helm, Tobias Roth and Mira Mezini. A Modular Soundness Theory for the Blackboard Analysis Architecture
  • Cyril Cohen, Enzo Crance and Assia Mahboubi. Trocq: Proof Transfer for Free, With or Without Univalence
  • Raphaël Monat, Aymeric Fromherz and Denis Merigoux. Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
  • Hiroya Fujinami and Ichiro Hasuo. Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping
  • Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni. Monadic Intersection Types, Relationally
  • Andrea Colledan and Ugo Dal Lago. Circuit Width Estimation via Effect Typing and Linear Dependency
  • Daniel Lundén, Lars Hummelgren, Jan Kudlicka, Oscar Eriksson and David Broman. Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
  • Shachar Itzhaky, Sharon Shoham and Yakir Vizel. Hyperproperty Verification as CHC Satisfiability
  • Théo Laurent, Meven Lennon-Bertrand and Kenji Maillard. Definitional Functoriality for Dependent (Sub)Types
  • Anders Ågren Thuné, Kazutaka Matsuda and Meng Wang. Reconciling Partial and Local Invertibility
  • Loïc Pujet and Nicolas Tabareau. Observational Equality Meets CIC
  • Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix. On the Hardness of Analyzing Quantum Programs Quantitatively
  • Yotam Dvir, Ohad Kammar and Ori Lahav. A Denotational Approach to Release-Acquire Concurrency
  • Pierre Lermusiaux and Benoit Montagu. Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation
  • Thiago Felicissimo. Generic Bidirectional Typing for Dependent Type Theories
  • Sam Lindley, Cristina Matache, Sean Moss, Sam Staton, Nicolas Wu and Zhixuan Yang. Scoped Effects as Parameterized Algebraic Theories
  • Elaine Li, Felix Stutz and Thomas Wies. Deciding Subtyping for Asynchronous Multiparty Sessions
  • Luis Caires and Bernardo Toninho. The Session Abstract Machine
FASE
  • Lucas Sakizloglou, Holger Giese and Leen Lambers. Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models
  • Margarita Capretto, Martin Ceresa and Cesar Sanchez. Monitoring the Future of Smart Contracts
  • Omar Al-Bataineh. Invariant-based Program Repair
  • Jan H. Boockmann and Gerald Luettgen. Comprehending Object State via Dynamic Class Invariant Learning
  • Yliès Falcone, Gwen Salaün and Ahang Zuo. Probabilistic Runtime Enforcement of Executable BPMN Processes
  • Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg and Mariëlle Stoelinga. Fuzzy quantitative attack tree analysis
  • Cedric Richter and Heike Wehrheim. Can ChatGPT support software verification?
  • Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang and Zhiping Shi. Refinement Verification of OS Services based on a Verified Preemptive Microkernel
  • He Xu, Sven Schneider and Holger Giese. Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems
  • Téo Bernier, Yani Ziani, Nikolai Kosmatov and Frédéric Loulergue. Combining Deductive Verification with Shape Analysis
  • Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura, Vasco Manquinho and Ruben Martins. Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation
  • Geunyeol Yu, Seunghyun Chae, Kyungmin Bae and Sungkun Moon. Formal Specification of Trusted Execution Environment APIs
  • Liushan Chen, Yu Pei, Mingyang Wan, Zhihui Fei, Tao Liang and Guojun Ma. Smart Issue Detection for Large-Scale Online Service Systems Using Multi-Channel Data
  • Dré van Oorschot, Marieke Huisman and Ömer Şakar. First Steps towards Deductive Verification of LLVM IR
FoSSaCS
  • Pete Austin, Sougata Bose and Patrick Totzke. Parity Games on Temporal Graphs
  • Philip Saville. Clones, Closed Categories, and Combinatory Logic
  • Bart Jacobs. Drawing from an Urn is Isometric
  • Patrick Baillot, Ugo Dal Lago, Cynthia Kop and Deivid Vale. On Basic Feasible Functionals and the Interpretation Method
  • Andrei Draghici, Christoph Haase and Andrew Ryzhikov. Reachability in Fixed VASS: Expressiveness and Lower Bounds
  • Daniel Hausmann, Nir Piterman, Irmak Saglam and Anne-Kathrin Schmuck. Fair Omega-regular Games
  • Orna Kupferman, Ofer Leshkowitz and Naama Shamash Halevy. Synthesis with Privacy Against an Observer
  • Dario Stein and Richard Samuelson. Towards a Compositional Framework for Convex Analysis (with Applications to Probability Theory)
  • Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas and Henning Urbat. Logical Predicates in Higher-Order Mathematical Operational Semantics
  • Fabian Birkmann, Stefan Milius and Henning Urbat. Monoidal Extended Stone Duality
  • Jesse Comer and Balder ten Cate. Craig Interpolation for Decidable First-Order Fragments
  • Beniamino Accattoli and Adrienne Lancelot. Light Genericity
  • Jan-Christoph Kassing, Florian Frohn and Jürgen Giesl. From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
  • Valentin Blot, Gilles Dowek, Thomas Traversié and Théo Winterhalter. From Rewrite Rules to Axioms in the lambdaPi-Calculus Modulo Theory
  • Laurent Doyen, Pranshu Gaba and Shibashis Guha. Stochastic Window Mean-payoff Games
  • Lucie Guillou, Corto Mascle and Nicolas Waldburger. Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
  • Philipp Czerner, Javier Esparza and Valentin Krasotin. A Resolution-Based Interactive Proof System for UNSAT
  • Luca Geatti, Alessio Mansutti and Angelo Montanari. Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems
  • Alejandro Villoria, Henning Basold and Alfons Laarman. Enriching Diagrams with Algebraic Operations
  • Daniel Hausmann, Mathieu Lehaut and Nir Piterman. Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
  • Shaull Almagor and Neta Dafni. Determinization of Integral Discounted-Sum Automata is Decidable
  • Shaull Almagor, Guy Avni, Henry Sinclair-Banks and Asaf Yeshurun. Dimension-Minimality and Primality of Counter Nets
  • Aditya Prakash. Checking History-Determinism is NP-hard for Parity Automata
  • Marek Jankola and Jan Strejček. Tighter Construction of Tight Büchi Automata
TACAS

Regular Research Papers

  • Mayank Solanki, Prantik Chatterjee, Akash Lal and Subhajit Roy. Accelerated Bounded Model Checking Using Interpolation Based Summaries
  • Satya Prakash Nayak and Anne-Kathrin Schmuck. Most General Winning Secure Equilibria Synthesis in Graph Games
  • Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot and Sebastian Junges. Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
  • Marijn Heule and Manfred Scheucher. Happy ending: An empty hexagon in every set of 30 points
  • Leonardo Lima, Jonathan Huerta Y Munive and Dmitriy Traytel. Explainable Online Monitoring of Metric First-Order Temporal Logic
  • Yubo Cai and Gleb Pogudin. Dissipative quadratizations of polynomial ODE systems
  • S. Akshay, Eliyahu Basa, Dror Fried and Supratik Chakraborty. On Dependent Variables in Reactive Synthesis
  • Lukas Westhofen, Christian Neurohr, Daniel Neider and Jean Christoph Jung. Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains
  • Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
  • Xiyue Zhang, Benjie Wang and Marta Kwiatkowska. Provable Preimage Under-Approximation for Neural Networks
  • Laura Bocchi, Andy King and Maurizio Murgia. Asynchronous Subtyping by Trace Relaxation
  • Paul Fiterau-Brostean, Simon Dierl, Falk Howar, Bengt Jonsson, Konstantinos Sagonas and Fredrik Tåquist. Scalable Tree-based Register Automata Learning
  • Nishant Rodrigues, Mircea Sebe, Xiaohong Chen and Grigore Rosu. A Logical Treatment of Finite Automata
  • Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán and Yon Shin Teo. A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation
  • Abhishek Kr Singh and Ori Lahav. Decidable Verification under Localized Release-Acquire Concurrency
  • Antonio Jiménez-Pastor, Kim Guldstrand Larsen, Mirco Tribastone and Max Tschaikowski. Forward and Backward Constrained Bisimulations for Quantum Circuits
  • Rüdiger Ehlers and Ayrat Khalimov. Fully Generalized Reactivity(1) Synthesis
  • Aditi Kabra, Jonathan Laurent, Stefan Mitsch and André Platzer. CESAR: Control Envelope Synthesis via Angelic Refinements
  • Raven Beutner. Automated Software Verification of Hyperliveness
  • Martin Jonáš, Jan Strejček, Marek Trtík and Lukáš Urban. Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage
  • Muhammad Osama and Anton Wijs. Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking
  • Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar and Florian Zuleger. Deciding Boolean Separation Logic via Small Models
  • Rupak Majumdar, Irmak Saglam and K. S. Thejaswini. Rabin Games and Colourful Universal Trees
  • Loes Kruger, Sebastian Junges and Jurriaan Rot. Small Test Suites for Active Automata Learning
  • Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky and Stefanie Mohr. Learning Explainable and Better Performing Representations of POMDP Strategies
  • Mohit Tekriwal, Avi-Tachna Fram, Jean-Baptiste Jeannin, Manos Kapritsos and Dimitra Panagou. Formally verified asymptotic consensus in robust networks
  • Anna Blume Jakobsen, Rasmus Skibdahl Melanchton Jorgensen, Andreas Pavlogiannis and Jaco van de Pol. Fast Symbolic Computation of Bottom SCCs
  • Guy Avni, Kaushik Mallik and Suman Sadhukhan. Auction-Based Scheduling
  • Dong Xu, Nusrat Jahan Mozumder, Hai Duong and Matthew Dwyer. Training for Verification: Increasing Neuron Stability to Scale DNN Verification
  • Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike and John Backes. DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
  • Florian Furbach, Parosh Aziz Abdulla, Mohamed Faouzi Atig and Shashwat Garg. Verification under TSO with an infinite Data Domain
  • Sumanth Prabhu, Deepak D’Souza, Supratik Chakraborty, Venkatesh R and Grigory Fedyukovich. Weakest Precondition Inference for Non-Deterministic Linear Array Programs
  • Hari Govind Vediramana Krishnan, Isabel Garcia-Contreras, Sharon Shoham and Arie Gurfinkel. Speculative SAT modulo SAT
  • Thibault Hilaire, David Ilcinkas and Jérôme Leroux. A State-of-the-Art Karp-Miller Algorithm Certified in Coq
  • Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga and Nils Jansen. CTMCs with Imprecisely Timed Observations

Case Study Papers

  • Lukas Koenig, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Kueperkoch, Dennis Fassbender and Michael Hanselmann. Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
  • Leping Zhang, Yongwang Zhao and Jianxin Li. A Comprehensive Specification and Verification of the L4 Microkernel API
  • Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler and Sascha Witt. Formally Verifying an Efficient Sorter

Tool Demo Papers

  • Md Solimul Chowdhury, Cayden Codel and Marijn Heule. TaSSAT: Transferring and Sharing in SAT
  • Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč. Z3-Noodler: An Automata-based String Solver
  • Mertcan Temel. VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification
  • Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov. Automate where Automation Fails: Proof Strategies for Frama-C/WP

Regular Tool Papers

  • Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci and Jaco van de Pol. On-The-Fly Algorithm for Reachability in Parametric Timed Games
  • Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee and Nils Sirrenberg. Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers
  • Matthias Cosler, Christopher Hahn, Ayham Omar and Frederik Schmitt. NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis
  • Nils Husung, Clemens Dubslaff, Holger Hermanns and Maximilian Alexander Köhl. OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust
  • Michalis Kokologiannakis, Viktor Vafeiadis and Rupak Majumdar. Enhancing GenMC’s Usability and Performance
  • David Chocholatý, Tomas Fiedor, Vojtěch Havlena, Lukáš Holík, Martin Hruska, Ondrej Lengal and Juraj Síč. Mata: A Fast and Simple Finite Automata Library
  • Tom van Dijk, Feije van Abbema and Naum Tomov. Knor: reactive synthesis using Oink
  • Cyrille Valentin Artho, Pavel Parizek, Daohan Qu, Varadraj Galgali and Pu Yi. JPF: From 2003 to 2023
  • Kadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo and Dongjie He. SootUp: A Redesign of the Soot Static Analysis Framework
  • Lars B. van den Haak, Anton Wijs, Marieke Huisman and Mark van den Brand. HaliVer: Deductive Verification and Scheduling Languages Join Forces
  • Hanna Lachnitt, Cesare Tinelli, Andrew Reynolds, Andres Noetzli, Haniel Barbosa, Leni Aniva, Clark Barrett and Mathias Fleury. IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL