Programme

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
  • 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
  • Momoko Hattori, Naoki Kobayashi and Ryosuke Sato. Gradual Tensor Shape Checking
  • 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
  • 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
  • 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
  • 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