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