Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Wednesday 15 April
10:00
Coffee Break
TACAS: Automata
Room:
10:30
A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
Kyveli Doveri, Pierre Ganty and B Srivathsan.
10:50
Modular Attractor Acceleration in Infinite-State Games
Philippe Heim and Rayna Dimitrova.
11:10
Concurrent Permissive Strategy Templates
Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak and Anne-Kathrin Schmuck.
11:30
LTLf Learning Meets Boolean Set Cover
Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon and Pierre Vandenhove.
11:50
Faster Signature Refinement for Branching Bisimilarity Minimization
Jan J.M. Martens and Maurice Laveaux.
12:10
MightyPPL : Model Checking MITL with Past and Pnueli Modalities
Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya.
ESOP: Verification
Room:
10:30
Validating Quantum State Preparation Programs
Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett and Alex Potanin.
10:50
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Del Valle, Alexandra Silva and Marco Gaboardi.
11:10
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler.
11:30
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing
Philipp Schröer, Darion Haase and Joost-Pieter Katoen.
11:50
A Program Logic for Under-approximating Worst-case Resource Usage
Ziyue Jin and Di Wang.
12:10
Specification-Driven Generation of Summaries for Symbolic Execution
Rafael Gonçalves, Frederico Ramos, Pedro Adão and José Fragoso Santos.
FOSSACS: Lambda-Calculus, Program Semantics, Infinite Structures
Room:
10:30
Interaction Improvement
Adrienne Lancelot, Giulio Manzonetto, Guy McCusker and Gabriele Vanoni.
10:50
Lambda Galore
Mariangiola Dezani-Ciancaglini, Besik Dundua and Furio Honsell.
11:10
K Definitions as Matching Logic Theories, Formally
Xiaohong Chen, Horatiu Cheval, Dorel Lucanu and Grigore Rosu
11:30
Abstract Lipschitz Continuity: Combining Semantic and Quantitative Approximations
Marco Campion, Isabella Mastroeni, Michele Pasqua and Caterina Urban.
11:50
Composition Theorems for f-Differential Privacy
Annabelle McIver, Natasha Fernandes and Parastoo Sadeghi.
12:10
Karp's NP-complete problems over first-order definable structures
Aidan Healy and Bartek Klin.
SPIN
Chair:
Room:
10:30
Industry Day
Chair:
Room:
10:30
12:30
Lunch Break
13:00
ETAPS General Assembly
15:30
Tool Demos (with Coffee Break)
16:00
Coffee Break with Tool Demos
ESOP: Types
Room:
16:30
Lenses for Partially-Specified States
Kazutaka Matsuda, Minh Nguyen and Meng Wang.
16:50
In Cantor Space No One Can Hear You Stream
Martin Baillon, Assia Mahboubi and Pierre-Marie Pédrot.
17:10
Contextual Metaprogramming for Session Types
Pedro Ângelo, Atsushi Igarashi, Yuito Murase and Vasco T. Vasconcelos.
17:30
Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism
Patrycja Balik, Szymon Jędras and Piotr Polesiuk.
17:50
Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism
Hasti Toossi and Ningning Xie.
18:10
Auditing Rust Crates Effectively
Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan and Caleb Stanford.
18:20
Code Generation via Meta-programming in Dependently Typed Proof Assistants
Mathis Bouverot-Dupuis and Yannick Forster.
TACAS: Static Analysis & Program Verification
Room:
16:30
ReCheck: Automated Contextual Improvement Verifier for Functional Calculi across User-Defined Operational Semantics
Makoto Hamana and Kento Emoto
16:50
On Deciding Constant Runtime of Linear Loops
Florian Frohn, Jürgen Giesl, Peter Giesl and Nils Lommen.
17:10
Data Structure Analysis for Binaries
Sadra Bayat Tork, Nicholas Coughlin, Alicia Michael, James Tobler and Kirsten Winter
17:30
Integrating String Reasoning in Symbolic Execution of C Programs
Rachel Cleaveland and Clark Barrett.
17:50
Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Tree
Nat Karmios, Sacha-Elie Ayoun and Philippa Gardner.
18:10
Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities
Ali Rasim Kocal, Michael Schwarz, Simmo Saan and Helmut Seidl
AE Reports (30mins)
Chair:
Room:
16:30
Industry Day
Chair:
Room:
16:30
SPIN
Chair:
Room:
16:30
19:00
ETAPS Banquet