Programme of main conferences from Monday to Thursday. All times are listed in CET (GMT+1).
The programme will be announced soon, please stay tuned!
Accepted Papers
ESOP
more
Guillaume Allais. Builtin Types viewed as Inductive Families
Flavio Ascari, Roberto Bruni and Roberta Gori. Logics for extensional, locally complete analysis via domain refinements
Paulo Emílio de Vilhena and François Pottier. A Type System for Effect Handlers and Dynamic Labels
Michael Schwarz, Simmo Saan, Helmut Seidl, Julian Erhard and Vesal Vojdani. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces
Soline Ducousso, Sébastien Bardin and Marie-Laure Potet. Adversarial Reachability for Program-level Security Analysis
Alexander Knapp, Heribert Mühlberger and Bernhard Reus. Interpreting Knowledge-based Programs
Wenjia Ye and Bruno Oliveira. Pragmatic Gradual Polymorphism with References
Yuito Murase, Yuichi Nishiwaki and Atsushi Igarashi. Contextual Modal Type Theory with Polymorphic Contexts
Berk Cirisci, Constantin Enea and Suha Orhun Mutluergil. Quorum Tree Abstractions of Consensus Protocols
Matthew Alan Le Brun and Ornela Dardha. MAGπ: Types for Failure-Prone Communication
Diana Costa, Andreia Mordido, Diogo Poças and Vasco T. Vasconcelos. System $F^\mu_\omega$ with Context-free Session Types
June Wunder, Arthur Azevedo de Amorim, Patrick Baillot and Marco Gaboardi. Bunched Fuzz: Sensitivity for Vector Metrics
Todd Schmid, Tobias Kappé and Alexandra Silva. A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Farzaneh Derakhshan, Myra Dotzel, Milijana Surbatovich and Limin Jia. Modal crash types for intermittent computing
Pedro Rocha and Luis Caires. Safe Session-Based Concurrency with Shared Linear State
Su-Hyeon Kim, Youngwook Kim, Yo-Sub Han, Hyeonseung Im and Sang-Ki Ko. Automated Grading of Regular Expressions
Basim Khajwal, Luke Ong and Dominik Wagner. Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing
Liliane-Joy Dandy, Emmanuel Jeandel and Vladimir Zamdzhiev. Type-safe (Variational) Quantum Programming in Idris
Daniel Lundén, Gizem Çaylak, Fredrik Ronquist and David Broman. Automatic Alignment in Higher-Order Probabilistic Programming Languages
FASE
more
Eduard Kamburjan and Crystal Chang Din. Runtime Enforcement Using Knowledge Bases
Leandro Batista Ribeiro, Florian Lorber, Ulrik Nyman, Kim Guldstrand Larsen and Marcel Baunach. A Modeling Concept for Formal Verification of OS-Based Compositional Software
Jan Haltermann, Marie-Christine Jakobs, Cedric Richter and Heike Wehrheim. Parallel Program Analysis via Range Splitting
Giordano d’Aloisio, Antinisca Di Marco and Giovanni Stilo. Democratizing Quality-Based Machine Learning Development through Extended Feature Models
Zhe Li and Fei Xie. Concolic Testing of Front-end JavaScript
Simon Bliudze, Petra van den Bos, Marieke Huisman, Robert Rubbens and Larisa Safina. Verified JavaBIP: Deductive & Runtime Verification of JavaBIP Models (Tool paper)
Luiz Carvalho, Renzo Degiovanni, Matías Brizzio, Maxime Cordy, Nazareno Aguirre, Yves Le Traon and Mike Papadakis. ACoRe: Automated Goal-Conflict Resolution
Saba Gholizadeh Ansari, I. S. W. B. Prasetya, Davide Prandi, Fitsum Meshesha Kifetew, Frank Dignum, Mehdi Dastani and Gabriele Keller. Model-based Player Experience Testing with Emotion Pattern Verification
Joshua Dawes, Donghwan Shin and Domenico Bianculli. Towards Log Slicing (NIER paper)
Geanderson Santos, Amanda Santana, Gustavo Vale and Eduardo Figueiredo. Yet Another Model! A Study on Model’s Similarities for Defect and Code Smells
Thomas Neele and Matteo Sammartino. Compositional Automata Learning of Synchronous Systems
Divya Gopinath, Luca Lungeanu, Ravi Mangal, Corina Pasareanu, Siqi Xie and Huafeng Yu. Feature-Guided Analysis of Neural Networks (NIER paper)
Mariano Politano, Valeria Bengolea, Facundo Molina, Nazareno Aguirre, Marcelo Frias and Pablo Ponzio. Efficient Bounded Exhaustive Input Generation from Program APIs
Chukri Soueidi, Yliès Falcone and Antoine El-Hokayem. Opportunistic Monitoring of Multithreaded Programs
Sinem Getir Yaman, Charlie Burholt, Maddie Jones, Radu Calinescu and Ana Cavalcanti. Specification and Validation of Normative Rules for Autonomous Agents (Tool paper)
Marek Chalupa, Stefanie Muroya Lei, Fabian Muehlboeck and Thomas Henzinger. VAMOS: Middleware for Best-Effort Third-Party Monitoring
FoSSaCS
more
Mikhail Starchak. On the Existential Arithmetics with Addition and Bitwise Minimum
Gaëtan Douéneau-Tabot. Pebble minimization: the last theorems
Aliaume Lopez. Noetherian topologies defined via fixed-points
Zhibo Chen and Frank Pfenning. A Logical Framework with Higher-Order Rational (Circular) Terms
Benjamin Bordais, Patricia Bouyer and Stephane Le Roux. Subgame optimal strategies in finite concurrent games with prefix-independent objectives
Marco Bernardo and Sabina Rossi. Reverse Bisimilarity vs. Forward Bisimilarity
Filip Mazowiecki, Henry Sinclair-Banks and Karol Węgrzycki. Coverability in 2-VASS with One Unary Counter is in NP
Faezeh Labbaf, Hossein Hojjat, Jan Friso Groote and Mohammadreza Mousavi. Compositional Learning for Interleaving Parallel Automata
Emmanuel Hainry, Romain Péchoux and Mário Silva. A programming language characterizing quantum polynomial time
Aditya Prakash and K. S. Thejaswini. On History-Deterministic One-Counter Nets
William Cocke and Paul Attie. Model and Program Repair via Group Actions
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla and Nicolas Peltier. A Strict Constrained Superposition Calculus for Graphs
Pascal Baumann, Flavio D’Alessandro, Moses Ganardi, Oscar Ibarra, Ian McQuillan, Lia Schütze and Georg Zetzsche. Unboundedness problems for machines with reversal-bounded counters
Quang Loc Le and Xuan-Bach D. Le. An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
Danel Ahman. When programs have to watch paint dry
Lukáš Holík, Juraj Síč, Lenka Turoňová and Tomas Vojnar. Fast Matching of Regular Patterns with Synchronizing Counting
Rob van Glabbeek. Just Testing
Jérémy Dubut and Thorsten Wißmann. Weighted and Branching Bisimilarities from Generalized Open Maps
Max New and Daniel R. Licata. A Formal Logic for Formal Category Theory
Udi Boker and Guy Hefetz. On the Comparison of Discounted-Sum Automata with Multiple Discount Factors
Pedro H Azevedo de Amorim. A Higher-Order Language for Markov Kernels and Linear Operators
Ruben Turkenburg, Clemens Kupke, Jurriaan Rot and Ezra Schoen. Preservation and Reflection of Bisimilarity via Invertible Steps
Thomas A. Henzinger, Nicolas Mazzocchi and N. Ege Saraç. Quantitative Safety and Liveness
Daniel Hirschkoff, Guilhem Jaber and Enguerrand Prebet. Deciding contextual equivalence of nu-calculus with effectful contexts
Pedro Nora, Sergey Goncharov, Dirk Hofmann, Lutz Schröder and Paul Wild. Kantorovich Functors and Characteristic Logics for Behavioural Distances
Amgad Rady and Franck van Breugel. Explainability of Probabilistic Bisimilarity Distances for Labelled Markov Chains
TACAS
more
Petar Vukmirović, Jasmin Blanchette and Stephan Schulz. Extending a High-Performance Prover to Higher-Order Logic
Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak and Anne-Kathrin Schmuck. Computing Adequately Permissive Assumptions for Synthesis
Guy Amir, Davide Corsi, Raz Yerushalmi, Luca Marzari, Alessandro Farinelli, David Harel and Guy Katz. Verifying Learning-Based Robotic Navigation Systems: A Case Study
Ocan Sankur. Timed Automata Verification and Synthesis via Finite Automata Learning
Bastien Thomas and Ocan Sankur. PyLTA: A Verification Tool for Parameterized Distributed Algorithms
Oliver Kullmann and Ankit Shukla. Transforming quantified boolean formulas using biclique covers
Wan Fokkink, Martijn Goorden, Dennis Hendriks, Bert van Beek, Albert Hofkamp, Ferdie Reijnen, Pascal Etman, Lars Moormann, Asia van de Mortel-Fronczak, Michel Reniers, Koos Rooda, Bram van der Sanden, Ramon Schiffelers, Sander Thuijsman, Jeroen Verbakel and Han Vogel. Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit
Tobias Meggendorfer. Correct Approximation of Stationary Distribution
Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni and Roopsha Samanta. Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification
Bernardo Subercaseaux and Marijn Heule. The Packing Chromatic Number of the Infinite Square Grid is 15
Alexander Bentkamp, Ramon Fernández Mir and Jeremy Avigad. Verified reductions for optimization
Joao Cortes, Ines Lynce and Vasco Manquinho. New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization
Joseph E. Reeves, Benjamin Kiesl-Reiter and Marijn J.H. Heule. Propositional Proof Skeletons
Dawn Michaelson, Dominik Schreiber, Marijn Heule, Benjamin Kiesl-Reiter and Mike Whalen. Unsatisfiability Proofs for Distributed SAT Solvers
Naoki Kobayashi and Minchao Wu. Neural Network-Guided Synthesis of Recursive Functions
Wenji Fang and Hongce Zhang. WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification
Vojtěch Havlena, Ondrej Lengal, Yong Li, Barbora Šmahlíková and Andrea Turrini. Modular Mix-and-Match Complementation of Büchi automata
Yahui Song and Wei-Ngan Chin. Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm
Saksham Aggarwal, Alejandro Stuckey de la Banda, Henri Urpani, Luke Yang and Julian Gutierrez. A Matrix-Based Approach to Parity Games
Casper Abild Larsen, Simon Meldahl Schmidt, Jesper Steensgaard, Anna Blume, Jakobsen, Jaco van de Pol and Andreas Pavlogiannis. A Truly Symbolic Linear-Time Algorithm for SCC Decomposition
Véronique Bruyère, Guillermo Perez and Gaëtan Staquet. Validating Streaming JSON Documents With Learned VPAs
Tzu-Han Hsu, Cesar Sanchez, Sarai Sheinvald and Borzoo Bonakdarpour. Efficient Loop Conditions for Bounded Model Checking Hyperproperties
Xavier Denis and Jacques-Henri Jourdan. Specifying and Verifying Higher-order Rust Iterators
Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner and Cesar Sanchez. Bounded Model Checking for Asynchronous Hyperproperties
Kyveli Doveri, Pierre Ganty and Luka Hadzi-Djokic. Antichains Algorithms for the Inclusion Problem Between ω-VPL
Engel Lefaucheux, Joel Ouaknine, David Purser and Mohammadamin Sharifi. Model Checking Linear Dynamical Systems under Floating-point Rounding
Alessandro Cimatti, Sara Corfini, Luca Cristoforetti, Marco Di Natale, Alberto Griggio, Stefano Tonetta and Florian Barrau. EVA: a Tool for the Compositional Verification of AUTOSAR Models
Michaël Cadilhac and Guillermo Perez. Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability
Leonardo Lima, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel and Simon Yuan. Explainable Online Monitoring of Metric Temporal Logic
Rodrigo Otoni, Igor Konnov, Jure Kukovec, Patrick Eugster and Natasha Sharygina. Symbolic Model Checking for TLA+ Made Faster
Xuanxiang Huang, Martin Cooper, Antonio Morgado, Jordi Planes and Joao Marques-Silva. Feature Necessity & Relevancy in ML Classifier Explanations
Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen and Christoph Matheja. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Martin Mariusz Lester. CoPTIC: Constraint Programming Translated Into C
Tobias Winkler and Joost-Pieter Katoen. Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
Parosh A. Abdulla, Mohamad F. Atig, Stephan Spengler, Shankara N. Krishna, Florian Furbach, Adwait A. Godbole and Yacoub G. Hendi. Parameterized Verification under TSO with Data Types
Marck van der Vegt, Nils Jansen and Sebastian Junges. Robust Almost-Sure Reachability in Multi-Environment MDPs
Ramana Nagasamudram, Anindya Banerjee and David A. Naumann. The WhyRel Prototype for Relational Verification of Pointer Programs
Shahaf Bassan and Guy Katz. Towards Formal Approximated Minimal Explanations of Neural Networks
Ali Bajwa, Minjian Zhang, Rohit Chadha and Mahesh Viswanathan. Stack-Aware Hyperproperties
Pantazis Deligiannis, Aditya Senthilnathan, Fahad Nayyar, Chris Lovett and Akash Lal. Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote
Elvira Albert, Jesús Correas Fernández, Pablo Gordillo, Guillermo Román-Díez and Albert Rubio. Inferring Needless Write Memory Accesses on Ethereum Bytecode
Yuning Wang and He Zhu. Verification-guided Programmatic Controller Synthesis
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak. Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning
Bruno Andreotti, Hanna Lachnitt and Haniel Barbosa. Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format
Raven Beutner and Bernd Finkbeiner. AbaHyper: Sound and Complete Model Checking for HyperLTL
Maximilian Heisinger, Martina Seidl and Armin Biere. ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving
Philippe Heim and Rayna Dimitrova. Taming Large Bounds in Synthesis from Bounded-Liveness Specifications
Iason Marmanis, Michalis Kokologiannakis and Viktor Vafeiadis. Reconciling Preemption Bounding with DPOR
Mrudula Balachander, Emmanuel Filiot and Jean-Francois Raskin. LTL Reactive Synthesis with a Few Hints
Anton Wijs and Muhammad Osama. A GPU Tree Database for Many-Core Explicit State Space Exploration
Seung Hoon Park, Rekha Pai and Tom Melham. A Formal CHERI-C Semantics for Verification
Tobias Fuchs, Jakob Bach and Markus Iser. Active Learning for SAT Solver Benchmarking
Arnd Hartmanns, Sebastian Junges, Tim Quatmann and Maximilian Weininger. A Practitioner’s Guide to MDP Model Checking Algorithms
Jelle Bouma, Stijn de Gouw and Sung-Shik Jongmans. Multiparty Session Typing in Java, Deductively
Ameer Hamza and Grigory Fedyukovich. Lockstep Composition for Unbalanced Loops
Shengping Xiao, Chengyu Zhang, Jianwen Li and Geguang Pu. FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format
Roland Meyer, Thomas Wies and Sebastian Wolff. Make flows small again: revisiting the flow framework
Kalmer Apinis and Vesal Vojdani. Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis
Johannes Schoisswohl, Laura Kovacs, Giles Reger, Konstantin Korovin and Andrei Voronkov. ALASCA: Reasoning in Quantified Linear Arithmetic
Parosh Abdulla, Mohamed Faouzi Atig, Krishna S, Ashutosh Gupta and Omkar Tuppe. Optimal Stateless Model Checking for Causal Consistency
Dirk Beyer, Po-Chun Chien and Nian-Ze Lee. Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Converter
Xingwu Guo, Ziwei Zhou, Yueling Zhang, Guy Katz and Min Zhang. OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks