Programme
Programme of main conferences from Monday to Thursday. Best Paper candidates are highlighted in yellow and by asterisk.
Monday 24 April
8:45
Opening
Room: Auditorium
9:00
Thomas Henzinger: A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems (unifying talk)
Chair: Natasha Sharygina
Room: Auditorium
10:00
Coffee break
Room: Foyer + 44 lobby
TACAS: Model Checking I
Chair: Natasha Sharygina
Room: Auditorium
10:30
Bounded Model Checking for Asynchronous Hyperproperties
T. Hsu, B. Bonakdarpour, B. Finkbeiner, C. Sanchez
11:00
Model Checking Linear Dynamical Systems under Floating-point Rounding
E. Lefaucheux, J. Ouaknine, D. Purser, M. Sharifi
11:30
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
T. Hsu, C. Sanchez, S. Sheinvald, B. Bonakdarpour
12:00
Reconciling Preemption Bounding with DPOR
Iason Marmanis, Michalis Kokologiannakis and Viktor Vafeiadis
TACAS: Machine Learning/Neural Networks
Chair: Roderick Bloem
Room: 44-45/108
10:30
Feature Necessity & Relevancy in ML Classifier Explanations
X. Huang, M. Cooper, A. Morgado, J. Planes, J. Marques-Silva
11:00
Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks
Shahaf Bassan and Guy Katz
11:30
OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks
X. Guo, Z. Zhou, Y. Zhang, G. Katz, M. Zhang
12:00
Neural Network-Guided Synthesis of Recursive Functions
Naoki Kobayashi and Minchao Wu
ESOP: Static Analysis
Chair: Thomas Wies
Room: 44-54/109
10:30
Logics for extensional, locally complete analysis via domain refinements
Flavio Ascari, Roberto Bruni and Roberta Gori
11:00
Clustered Relational Thread-Modular Abstract Interpretation with Local Traces
Michael Schwarz, Simmo Saan, Helmut Seidl, Julian Erhard and Vesal Vojdani
11:30
Adversarial Reachability for Program-level Security Analysis
Soline Ducousso, Sébastien Bardin and Marie-Laure Potet
12:00
Automated Grading of Regular Expressions
Su-Hyeon Kim, Youngwook Kim, Yo-Sub Han, Hyeonseung Im and Sang-Ki Ko
FoSSaCS: Programming Languages
Chair:
Room: 44-45/106
10:30
When programs have to watch the paint dry
Danel Ahman
11:00
Deciding contextual equivalence of nu- calculus with effectful contexts
Daniel Hirschkoff, Guilhem Jaber and Enguerrand Prebet
11:30
Kantorovich Functors and Characteristic Logics for Behavioural Distances
Pedro Nora, Sergey Goncharov, Dirk Hofmann, Lutz Schröder and Paul Wild
12:00
A Logical Framework with Higher-Order Rational (Circular) Terms
Zhibo Chen and Frank Pfenning
12:30
Lunch
Room: Patio + Foyer
TACAS: Automata
Chair: Sriram Sankaranarayanan
Room: Auditorium
14:00
Modular Mix-and-Match Complementation of Büchi automata
V. Havlena, O. Lengal, Y. Li, B. Šmahlíková, A. Turrini
14:30
Validating Streaming JSON Documents With Learned VPAs
V. Bruyère, G. Perez, G. Staquet
15:00
Antichains Algorithms for the Inclusion Problem Between ω-VPL
K. Doveri, P. Ganty, L. Hadzi-Djokic
15:30
Stack-Aware Hyperproperties
A. Bajwa, M. Zhang, R. Chadha, M. Viswanathan
TACAS: SV-COMP
Chair: Dirk Beyer
Room: 24-25/405
14:00
Organization
Dirk Beyer
14:20
2LS
František Nečas
14:26
CPAchecker
Henrik Wachowitz
14:32
EBF
Fatimah Aljaafari
14:38
GDart-LLVM
Simon Dierl
14:44
Goblint
Simmo Saan
14:50
JBMC
Peter Schrammel
14:56
Korn
Gidon Ernst
15:02
LF-checker
Tong Wu
15:08
Mopsa
Raphaël Monat
15:14
Symbiotic-Witch 2
Paulína Ayaziová
15:20
Ultimate Automizer
Matthias Heizmann
15:26
Ultimate GemCutter
Dominik Klumpp
15:32
Ultimate Taipan
Frank Schüssele
15:38
VeriAbsL
Priyanka Darke
15:44
VeriFuzz
M. Raveemdra Kumar
ESOP: Type Systems
Chair: Sandrine Blazy
Room: 44-45/106
14:00
Pragmatic Gradual Polymorphism with References
Wenjia Ye and Bruno Oliveira
14:30
Gradual Tensor Shape Checking
Momoko Hattori, Naoki Kobayashi and Ryosuke Sato
15:00
Modal crash types for intermittent computing
Farzaneh Derakhshan, Myra Dotzel, Milijana Surbatovich and Limin Jia
15:30
Builtin Types viewed as Inductive Families
Guillaume Allais
FoSSaCS: Semantics
Chair:
Room: 44-45/108
14:00
A Higher-Order Language for Markov Kernels and Linear Operators
Pedro H Azevedo de Amorim
14:30
A Formal Logic for Formal Category Theory
Max New and Daniel R. Licata
15:00
A Strict Constrained Superposition Calculus for Graphs
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla and Nicolas Peltier
15:30
A programming language characterizing quantum polynomial time
Emmanuel Hainry, Romain Péchoux and Mário Silva
16:00
Coffee Break
Room: Foyer + 44 lobby
TACAS: Proofs
Chair: David Monniaux
Room: 44-45/108
16:30
Propositional Proof Skeletons
J. Reeves, B. Kiesl-Reiter, M. Heule
17:00
Unsatisfiability Proofs for Distributed Clause Sharing SAT Solvers*
D. Michaelson, D. Schreiber, M. Heule, B. Kiesl-Reiter, M. Whalen
17:30
Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format
B. Andreotti, H. Lachnitt, H. Barbosa
TACAS: SV-COMP
Chair: Dirk Beyer
Room: 24-25/405
16:30
SV-COMP Community Meeting
Dirk Beyer
Invited tutorial
Chair: Marieke Huisman
Room: Auditorium
18:00
Welcome Reception
Tuesday 25 April
9:00
Mooly Sagiv: Scaling Formal Verification to Realistic Code with Applications to DeFi Verification (ESOP invited talk)
Chair: Thomas Wies
Room: Auditorium
10:00
Coffee break
Room: Foyer + 44 lobby
TACAS: Constraint Solving/Blockchain
Chair: Sriram Sankaranarayanan
Room: Auditorium
10:30
The Packing Chromatic Number of the Infinite Square Grid is 15*
B. Subercaseaux, M. Heule
11:00
Active Learning for SAT Solver Benchmarking
T. Fuchs, J. Bach, M. Iser
11:30
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving
M. Heisinger, M. Seidl, Armin Biere
12:00
Inferring Needless Write Memory Accesses on Ethereum Bytecode
E. Albert, J. Correas, P. Gordillo, G. Román-Díez, A. Rubio
ESOP: Semantics and Type Theory
Chair: Luis Caires
Room: 44-45/106
10:30
Interpreting Knowledge-based Programs
Alexander Knapp, Heribert Mühlberger and Bernhard Reus
11:00
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Todd Schmid, Tobias Kappé and Alexandra Silva
11:30
Contextual Modal Type Theory with Polymorphic Contexts*
Yuito Murase, Yuichi Nishiwaki and Atsushi Igarashi
12:00
A Type System for Effect Handlers and Dynamic Labels*
Paulo Emílio de Vilhena and François Pottier
FoSSaCS: Counters
Chair:
Room: 44-45/108
10:30
On the Existential Arithmetics with Addition and Bitwise Minimum
Mikhail Starchak
11:00
Coverability in 2-VASS with One Unary Counter is in NP
Filip Mazowiecki, Henry Sinclair-Banks and Karol Węgrzycki
11:30
On History-Deterministic One-Counter Nets
Aditya Prakash and K. S. Thejaswini
12:00
Unboundedness problems for machines with reversal-bounded counters*
Pascal Baumann, Flavio D'Alessandro, Moses Ganardi, Oscar Ibarra, Ian McQuillan, Lia Schütze and Georg Zetzsche
Ask-Me-Anything
Chair:
Room: 24-25/405
10:30
Orna Kupferman: On Her Research
interviewed by Georgiana Caltais
11:00
Marieke Huisman: On Conference Organisation And Related Issues
interviewed by Eduard Kamburjan
11:30
Dirk Beyer and Andrzej Murawski: On Replicability
interviewed by Benjamin Kaminski
12:30
Lunch
Room: Patio + Foyer
TACAS: Markov Chains/Stochastic Control
Chair: Kim Larsen
Room: Auditorium
14:00
A Practitioner's Guide to MDP Model Checking Algorithms*
Arnd Hartmanns, Sebastian Junges, Tim Quatmann and Maximilian Weininger
14:30
Correct Approximation of Stationary Distribution
Tobias Meggendorfer
15:00
Robust Almost-Sure Reachability in Multi-Environment MDPs
Marck van der Vegt, Nils Jansen and Sebastian Junges
15:30
Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning
E. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, D. Wojtczak
TACAS: Verification I
Chair: Haniel Barbosa
Room: 44-45/108
14:00
A Formal CHERI-C Semantics for Verification
Seung Hoon Park, Rekha Pai and Tom Melham
14:30
Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm
Yahui Song and Wei-Ngan Chin
15:00
Parameterized Verification under TSO with Data Types
P. Abdulla, M.. Atig, S. Spengler, S. Krishna, F. Furbach, A. A. Godbole, Y. G. Hendi
15:30
Verifying Learning-Based Robotic Navigation Systems
Guy Amir, Davide Corsi, Raz Yerushalmi, Luca Marzari, Alessandro Farinelli, David Harel and Guy Katz
ESOP: Concurrency
Chair: Simon Gay
Room: 44-45/106
14:00
Quorum Tree Abstractions of Consensus Protocols
Berk Cirisci, Constantin Enea and Suha Orhun Mutluergil
14:30
MAGπ: Types for Failure-Prone Communication
Matthew Alan Le Brun and Ornela Dardha
15:00
Safe Session-Based Concurrency with Shared Linear State
Pedro Rocha and Luis Caires
15:30
System $F^mu_omega$ with Context-free Session Types
Diana Costa, Andreia Mordido, Diogo Poças and Vasco T. Vasconcelos
FoSSaCS: Bisimulation
Chair:
Room: 44-54/109
14:00
Reverse Bisimilarity vs. Forward Bisimilarity
Marco Bernardo and Sabina Rossi
14:30
Explainability of Probabilistic Bisimilarity Distances for Labelled Markov Chains
Amgad Rady and Franck van Breugel
15:00
Weighted and Branching Bisimilarities from Generalized Open Maps
Jérémy Dubut and Thorsten Wißmann
15:30
Preservation and Reflection of Bisimilarity via Invertible Steps
Ruben Turkenburg, Clemens Kupke, Jurriaan Rot and Ezra Schoen
16:00
Coffee break
Room: Foyer + 44 lobby
TACAS: Tool Demos
Chair: Sergio Mover
Room: 44-45/108
16:30
EVA: A Tool for the Compositional Verification of AUTOSAR Models
A. Cimatti, S. Corfini, L. Cristoforetti, M. Di Natale, A. Griggio, S. Tonetta, F. Barrau
16:45
PyLTA: A Verification Tool for Parameterized Distributed Algorithms
Bastien Thomas and Ocan Sankur
17:00
WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification
Wenji Fang and Hongce Zhang
17:15
FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format
S. Xiao, C. Zhang, J. Li, G. Pu
17:30
Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit
W. Fokkink, M. Goorden, D. Hendriks, B. Beek, A. Hofkamp, F. Reijnen, P. Etman, L. Moormann, A. Mortel-Fronczak, M. Reniers, K. Rooda, B. Sanden, R. Schiffelers, S. Thuijsman, J. Verbakel, H. Voge
17:45
Multiparty Session Typing in Java, Deductively
Jelle Bouma, Stijn de Gouw and Sung-Shik Jongmans
Invited Tutorial
Chair: Lenore Zuck
Room: Auditorium
Diversity and Inclusion Activities
Chair: Fabrice Kordon
Room: 44-45/106
16:30
Wednesday 26 April
9:00
Véronique Cortier: Electronic Voting: Design And Formal Verification (unifying talk)
Chair: Orna Kupferman
Room: Auditorium
10:00
Coffee break
Room: Foyer + 44 lobby
TACAS: Combinatorial Optimization / Theorem Proving
Chair: Haniel Barbosa
Room: Auditorium
10:30
New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization
J. Cortes, I. Lynce, V. Manquinho
11:00
Verified reductions for optimization
A. Bentkamp, R. Fernández Mir, J. Avigad
11:30
Specifying and Verifying Higher-order Rust Iterators
X. Denis, J. Jourdan
12:00
Extending a High-Performance Prover to Higher-Order Logic
P. Vukmirović, J. Blanchette, S. Schulz
TACAS: Tools (Regular Papers)
Chair: Alessandro Cimatti
Room: 44-45/108
10:30
The WhyRel Prototype for Relational Verification of Pointer Programs*
R. Nagasamudram, A. Banerjee, D. Naumann
11:00
Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Converter
D. Beyer, P. Chien, Nian-Ze Lee
11:30
CoPTIC: Constraint Programming Translated Into C
Martin Mariusz Lester
12:00
Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability
Michaël Cadilhac and Guillermo Perez
FASE: Requirements, Models and AI
Chair: Facundo Molina
Room: 44-54/109
10:30
ACoRe: Automated Goal-Conflict Resolution*
Luiz Carvalho, Renzo Degiovanni, Matías Brizzio, Maxime Cordy, Nazareno Aguirre, Yves Le Traon and Mike Papadakis
11:00
Democratizing Quality-Based Machine Learning Development through Extended Feature Models
Giordano d'Aloisio, Antinisca Di Marco and Giovanni Stilo
11:30
Compositional Automata Learning of Synchronous Systems
Thomas Neele and Matteo Sammartino
12:00
Feature-Guided Analysis of Neural Networks (NIER paper)
Divya Gopinath, Luca Lungeanu, Ravi Mangal, Corina Pasareanu, Siqi Xie and Huafeng Yu
12:15
Specification and Validation of Normative Rules for Autonomous Agents (Tool paper)*
Sinem Getir Yaman, Charlie Burholt, Maddie Jones, Radu Calinescu and Ana Cavalcanti
FoSSaCS: Formal Languages
Chair:
Room: 44-45/106
10:30
Quantitative Safety and Liveness
Thomas A. Henzinger, Nicolas Mazzocchi and N. Ege Saraç
11:00
On the Comparison of Discounted-Sum Automata with Multiple Discount Factors
Udi Boker and Guy Hefetz
11:30
Fast Matching of Regular Patterns with Synchronizing Counting
Lukáš Holík, Juraj Síč, Lenka Turoňová and Tomas Vojnar
12:00
Compositional Learning for Interleaving Parallel Automata
Faezeh Labbaf, Hossein Hojjat, Jan Friso Groote and Mohammadreza Mousavi
SPIN (co-located)
Chair: Max Tschaikowski
Room: 25-26/105
11:30
Efficient Implementation of LIMDDs for Quantum Circuit Simulation
Lieuwe Vinkhuijzen, Thomas Grurl, Stefan Hillmich, Sebastiaan Brand, Robert Wille and Alfons Laarman
12:00
ParaGnosis: A Tool for Parallel Knowledge Compilation
Giso Dal, Alfons W. Laarman and Peter J.F. Lucas
12:30
Lunch
Room: Patio + Foyer
13:00
ETAPS General Assembly
Room: Auditorium
TACAS: Synthesis I
Chair: Cesar Sanchez
Room: Auditorium
14:00
Verification-guided Programmatic Controller Synthesis
Yuning Wang and He Zhu
14:30
Computing Adequately Permissive Assumptions for Synthesis
Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak and Anne-Kathrin Schmuck
15:00
Taming Large Bounds in Synthesis from Bounded-Liveness Specifications
Philippe Heim and Rayna Dimitrova
15:30
Lockstep Composition for Unbalanced Loops
Ameer Hamza and Grigory Fedyukovich
ESOP: Probabilistic and Quantum Programming
Chair: Benjamin Kaminski
Room: 44-45/108
14:00
Type-safe (Variational) Quantum Programming in Idris
Liliane-Joy Dandy, Emmanuel Jeandel and Vladimir Zamdzhiev
14:30
Bunched Fuzz: Sensitivity for Vector Metrics
June Wunder, Arthur Azevedo de Amorim, Patrick Baillot and Marco Gaboardi
15:00
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing
Basim Khajwal, Luke Ong and Dominik Wagner
15:30
Automatic Alignment in Higher-Order Probabilistic Programming Languages*
Daniel Lundén, Gizem Çaylak, Fredrik Ronquist and David Broman
FASE: Runtime Monitoring & Enforcement
Chair: Heike Wehrheim
Room: 44-54/109
14:00
Opportunistic Monitoring of Multithreaded Programs
Chukri Soueidi, Yliès Falcone and Antoine El-Hokayem
14:30
VAMOS: Middleware for Best-Effort Third-Party Monitoring
Marek Chalupa, Stefanie Muroya Lei, Fabian Muehlboeck and Thomas Henzinger
15:00
Runtime Enforcement Using Knowledge Bases
Eduard Kamburjan and Crystal Chang Din
FoSSaCS: Formal methods
Chair:
Room: 44-45/106
14:00
Pebble minimization: the last theorems
Gaëtan Douéneau-Tabot
14:30
Noetherian topologies defined via fixed-points
Aliaume Lopez
15:00
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
Quang Loc Le and Xuan-Bach D. Le
SPIN (co-located)
Chair: Arnd Hartmanns
Room: 25-26/105
15:00
Model Checking Futexes
Hugues Evrard and Alastair Donaldson
15:30
Sound Concurrent Traces for Online Monitoring
Chukri Soueidi and Yliès Falcone
16:00
Coffee Break
Room: Foyer + 44 lobby
SPIN (co-located)
Chair: Alfons Laarman
Room: 25-26/105
16:30
Elimination of Detached Regions in Dependency Graph Verification
Peter Gjøl Jensen, Kim Guldstrand Larsen, Jiri Srba and Nikolaj Jensen Ulrik
17:00
Potency-Based Heuristic Search with Randomness for Explicit Model Checking
Emil G. Henriksen, Alan M. Khorsid, Esben Nielsen, Theodor Risager, Jiri Srba, Adam M. Stuck and Andreas S. Sørensen
17:20
GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data
Anton Wijs and Muhammad Osama
TOOLympics
Room: Auditorium
16:30
Introduction
Dirk Beyer, Fabrice Kordon, Arnd Hartmanns
16:40
CHC-COMP
Hossein Hojjat
16:46
MCC
Fabrice Kordon
16:52
QComp
Arnd Hartmanns
16:58
ARCH-COMP
Arnd Hartmanns
17:04
RERS
Falk Howar
17:10
SL-COMP
Mihaela Sighireanu
17:16
SV-COMP
Dirk Beyer
17:22
Test-Comp
Dirk Beyer
17:28
VerifyThis
Gidon Ernst
17:34
VT-LTC
Gidon Ernst
19:00
Banquet
Thursday 27 April
9:00
Sven Apel: Brains on Code: Towards a Neuroscientific Foundation of Program Comprehension (FASE invited talk)
Chair: Leen Lambers
Room: Auditorium
10:00
Coffee break
Room: Foyer + 44 lobby
TACAS: Verification II
Chair: Dirk Beyer
Room: Auditorium
10:30
Make flows small again: revisiting the flow framework
Roland Meyer, Thomas Wies and Sebastian Wolff
11:00
ALASCA: Reasoning in Quantified Linear Arithmetic
Johannes Schoisswohl, Laura Kovacs, Giles Reger, Konstantin Korovin and Andrei Voronkov
11:30
A Matrix-Based Approach to Parity Games
Saksham Aggarwal, Alejandro Stuckey de la Banda, Henri Urpani, Luke Yang and Julian Gutierrez
12:00
A GPU Tree Database for Many-Core Explicit State Space Exploration
Anton Wijs and Muhammad Osama
TACAS: Graphs/Probabilistic Systems
Chair: Natasha Sharygina
Room: 44-45/108
10:30
A Truly Symbolic Linear-Time Algorithm for SCC Decomposition
Casper Abild Larsen, Simon Meldahl Schmidt, Jesper Steensgaard, Anna Blume Jakobsen, Jaco van de Pol and Andreas Pavlogiannis
11:00
Transforming quantified boolean formulas using biclique covers
Oliver Kullmann and Ankit Shukla
11:30
Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
T. Winkler, Joost-Pieter Katoen
12:00
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
K. Batz, M. Chen, S. Junges, B. Kaminski, Joost-Pieter Katoen, Christoph Matheja
FASE: Analysis & Verification
Chair: Eduard Kamburjan
Room: 44-54/109
10:30
Parallel Program Analysis via Range Splitting
Jan Haltermann, Marie-Christine Jakobs, Cedric Richter and Heike Wehrheim
11:00
Yet Another Model! A Study on Model's Similarities for Defect and Code Smells
Geanderson Santos, Amanda Santana, Gustavo Vale and Eduardo Figueiredo
11:30
A Modeling Concept for Formal Verification of OS-Based Compositional Software
Leandro Batista Ribeiro, Florian Lorber, Ulrik Nyman, Kim Guldstrand Larsen and Marcel Baunach
12:00
Towards Log Slicing (NIER paper)
Joshua Dawes, Donghwan Shin and Domenico Bianculli
12:15
JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java (Tool paper)
Simon Bliudze, Petra van den Bos, Marieke Huisman, Robert Rubbens and Larisa Safina
FoSSaCS: Verification
Chair:
Room: 44-45/106
10:30
Just Testing
Rob van Glabbeek
11:00
Model and Program Repair via Group Actions
William Cocke and Paul Attie
11:30
Subgame optimal strategies in finite concurrent games with prefix-independent objectives
Benjamin Bordais, Patricia Bouyer and Stephane Le Roux.
SPIN (co-located)
Chair: Sergio Mover
Room: 25-26/105
11:30
Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks
Bryant Israelsen, Landon Taylor and Zhen Zhang
12:00
Accelerating black box testing with light-weight learning
Roi Fogler, Itay Cohen and Doron Peled
12:30
Lunch
Room: Patio + Foyer
TACAS: Model Checking II
Chair: Sriram Sankaranarayanan
Room: Auditorium
14:00
Optimal Stateless Model Checking for Causal Consistency
Parosh Abdulla, Mohamed Faouzi Atig, Krishna S, Ashutosh Gupta and Omkar Tuppe
14:30
Symbolic Model Checking for TLA+ Made Faster
R. Otoni, I. Konnov, J. Kukovec, P. Eugster, N. Sharygina
15:00
AutoHyper: Explicit-State Model Checking for HyperLTL*
R. Beutner and B. Finkbeiner
FASE: Testing
Chair: Andrzej Wąsowski
Room: 44-45/108
14:00
Efficient Bounded Exhaustive Input Generation from Program APIs
Mariano Politano, Valeria Bengolea, Facundo Molina, Nazareno Aguirre, Marcelo Frias and Pablo Ponzio
14:30
Model-based Player Experience Testing with Emotion Pattern Verification
Saba Gholizadeh Ansari, I. S. W. B. Prasetya, Davide Prandi, Fitsum Meshesha Kifetew, Frank Dignum, Mehdi Dastani and Gabriele Keller
15:00
Concolic Testing of Front-end JavaScript
Zhe Li and Fei Xie
Awards
Chair: Marieke Huisman
Room: 44-45/106
14:00
Test-of-Time Award
Explicit-State Software Model Checking Based on CEGAR and Interpolation, by Dirk Beyer and Stefan Löwe
14:30
Dissertation Award
Pushing the Barriers in Controller Synthesis for Cyber-Physical Systems, by Kaushik Mallik
15:00
Test-of-Time Tool Award
CADP: Construction and Analysis of Distributed Processes, by Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
SPIN (co-located)
Chair: Matthias Heizmann
Room: 25-26/105
15:00
WikiCoder: Learning to Write Knowledge-Powered Code
Théo Matricon, Nathanaël Fijalkow and Gaëtan Margueritte
15:30
Provable Correct and Adaptive Simplex Architecture for Bounded-Liveness Properties
Benedikt Maderbacher, Stefan Schupp, Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Bettina Könighofer
16:00
Coffee break
Room: Foyer + 44 lobby
TACAS: Monitoring/Program Analysis
Chair: Jan Kofroň
Room: Auditorium
16:30
Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote*
P. Deligiannis, A. Senthilnathan, F. Nayyar, C. Lovett, A. Lal
17:00
Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis
Kalmer Apinis and Vesal Vojdani
17:30
Explainable Online Monitoring of Metric Temporal Logic
L. Lima, A. Herasimau, M. Raszyk, D. Traytel, S. Yuan
TACAS: Synthesis II
Chair: Cesar Sanchez
Room: 44-45/108
16:30
Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification*
N. Jaber, C. Wagner, S. Jacobs, M. Kulkarni, R. Samanta
17:00
LTL Reactive Synthesis with a Few Hints
M. Balachander, E. Filiot, Jean-Francois Raskin
17:30
Timed Automata Verification and Synthesis via Finite Automata Learning
Ocan Sankur
FASE: Test-Comp
Chair: Dirk Beyer
Room: 24-25/405
16:30
Organization
Dirk Beyer
16:50
FuSeBMC_IA
Fedor Shmarov
17:05
Legion
Gidon Ernst
17:20
VeriFuzz
M. Raveemdra Kumar
17:35
Community Meeting
Dirk Beyer
Accepted Papers
ESOP
moreless
- 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
moreless
- 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
moreless
- 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
moreless
- 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