Programme
Programme of main conferences from Monday to Thursday. Best Paper candidates are highlighted in yellow and by asterisk.
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