Programme

Programme of main conferences from Monday to Thursday. Best Paper candidates are highlighted in yellow and by asterisk.

Wednesday 10 April

10:00
Coffee Break
TACAS: Software Verification
Chair: Tomáš Vojnar
Room: Hollenfels
10:30
Accelerated Bounded Model Checking Using Interpolation Based Summaries
Mayank Solanki, Prantik Chatterjee, Akash Lal and Subhajit Roy
11:00
Weakest Precondition Inference for Non-Deterministic Linear Array Programs
Sumanth Prabhu, Deepak D'Souza, Supratik Chakraborty, Venkatesh R and Grigory Fedyukovich
11:30
Automated Software Verification of Hyperliveness
Raven Beutner
12:00
A Comprehensive Specification and Verification of the L4 Microkernel API
Leping Zhang, Yongwang Zhao and Jianxin Li
ESOP: Domain-Specific Languages
Chair: Josh Ko
Room: Schengen II
10:30
Circuit Width Estimation via Effect Typing and Linear Dependency
Andrea Colledan and Ugo Dal Lago
11:00
Reconciling Partial and Local Invertibility
Anders Ågren Thuné, Kazutaka Matsuda and Meng Wang
11:30
On the Hardness of Analyzing Quantum Programs Quantitatively
Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix
12:00
Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping
Hiroya Fujinami and Ichiro Hasuo
FoSSaCS: Automata and Synthesis
Chair: Bart Jacobs
Room: Diekirch-Echternach-Fischbach
10:30
Determinization of Integral Discounted-Sum Automata is Decidable
Shaull Almagor and Neta Dafni
11:00
Checking History-Determinism is NP-hard for Parity Automata
Aditya Prakash
11:30
Tighter Construction of Tight Büchi Automata
Marek Jankola and Jan Strejček
12:00
Synthesis with Privacy Against an Observer
Orna Kupferman, Ofer Leshkowitz and Naama Shamash Halevy
Spin: Software Verification
Chair: Thomas Neele
Room: Schengen I
10:30
Taming the AI Monster: Monitoring of Individual Fairness for Effective Human Oversight (keynote)
Holger Hermanns
11:30
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants*
Dirk Beyer, Po-Chun Chien and Nian-Ze Lee
12:00
Test-Case Generation with Automata-based Software Model Checking
Max Barth and Marie-Christine Jakobs
12:30
Lunch
13:00
ETAPS General Assembly
TACAS: Probabilistic Systems
Chair: Kim Larsen
Room: Hollenfels
14:00
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains*
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler
14:30
CTMCs with Imprecisely Timed Observations
Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga and Nils Jansen
15:00
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot and Sebastian Junges
15:30
Learning Explainable and Better Performing Representations of POMDP Strategies
Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky and Stefanie Mohr
ESOP: Bidirectional typing / Session types
Chair: Ugo Dal Lago
Room: Schengen II
14:00
A formal treatment of bidirectional typing
Liang-Ting Chen and Hsiang-Shang Ko
14:30
Generic bidirectional typing for dependent type theories
Thiago Felicissimo
15:00
The Session Abstract Machine
Luis Caires and Bernardo Toninho
15:30
Deciding Subtyping for Asynchronous Multiparty Sessions
Elaine Li, Felix Stutz and Thomas Wies
FoSSaCS: Types and Programming Languages
Chair: James Worrell
Room: Diekirch-Echternach-Fischbach
14:00
From Rewrite Rules to Axioms in the lambdaPi-Calculus Modulo Theory
Valentin Blot, Gilles Dowek, Thomas Traversié and Théo Winterhalter
14:30
Light Genericity
Beniamino Accattoli and Adrienne Lancelot
15:00
Logical Predicates in Higher-Order Mathematical Operational Semantics
Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas and Henning Urbat
15:30
On Basic Feasible Functionals and the Interpretation Method
Patrick Baillot, Ugo Dal Lago, Cynthia Kop and Deivid Vale
Spin: Anniversary Track
Chair: Anton Wijs
Room: Schengen I
14:00
The Spin on Spin (keynote)
Gerald Holzmann
15:00
Two Decades of Industrializing Formal Verification: The Reactis Story
Rance Cleaveland, David Hansel, Steve Sims and Scott Smolka
15:30
Automated Reasoning in Quantum Circuit Compilation
Dimitrios Thanos, Alejandro Villoria, Sebastiaan Brand, Arend-Jan Quist, Jingyi Mei, Tim Coopmans and Alfons Laarman
Tool demo session
Room: Europe B
14:00
16:00
Coffee break
TACAS: Simulations
Chair: Javier Esparza
Room: Hollenfels
16:30
Dissipative quadratizations of polynomial ODE systems
Yubo Cai and Gleb Pogudin
17:00
Forward and Backward Constrained Bisimulations for Quantum Circuits
Antonio Jiménez-Pastor, Kim Guldstrand Larsen, Mirco Tribastone and Max Tschaikowski
17:30
A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation
Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán and Yon Shin Teo
ESOP: Dependent Types
Chair: Benoit Montagu
Room: Schengen II
16:30
Observational Equality Meets CIC
Loïc Pujet and Nicolas Tabareau
17:00
Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance and Assia Mahboubi
17:30
Definitional Functoriality for Dependent (Sub)Types
Théo Laurent, Meven Lennon-Bertrand and Kenji Maillard
TACAS: Neural Networks
Chair: Arie Gurfinkel
Room: Diekirch-Echternach-Fischbach
16:30
Provable Preimage Under-Approximation for Neural Networks
Xiyue Zhang, Benjie Wang and Marta Kwiatkowska
17:00
Training for Verification: Increasing Neuron Stability to Scale DNN Verification
Dong Xu, Nusrat Jahan Mozumder, Hai Duong and Matthew Dwyer
17:30
NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis
Matthias Cosler, Christopher Hahn, Ayham Omar and Frederik Schmitt
Spin: Automated Reasoning
Chair: Alfons Laarman
Room: Schengen I
16:30
Random Access on Narrow Decision Diagrams in External Memory
Steffan Christ Sølvsten, Casper Moldrup Rysgaard and Jaco van de Pol
17:00
Solving Constrained Horn Clauses as C Programs with CHC2C
Levente Bajczi and Vince Molnár
Programme in PDF for print
Full Programme