Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Wednesday 15 April
09:00
Monika Henzinger: Guarding Privacy Over Time: Challenges and Solutions in Continuous Data Observation
Chair: Laura Kovács
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: Automata
Room: Expo Area
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: Sala Berlino
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: Sala Londra
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: Sala Parigi
10:30
Industry Day
Chair: Nikolai Kosmatov
Room: Sala Madrid
10:30
Weathering the Weather: The Storms Gathering Around the Development of Safety-Critical Systems
Chris Hobbs (Consultant)
11:15
Safe Agile: A Safety Strategy for Agile Development Strategy for Spacecrafts or Space robots
Thomas Chowdhury (MDA Space)
12:00
Temporal specification languages in industrial hardware verification
Simon Jantsch (Siemens EDA)
12:30
Lunch Break
Room: Expo Area
13:00
ETAPS General Assembly
Room: Sala 500
14:00
Industry Day
Chair: Nikolai Kosmatov
Room: Sala Madrid
14:00
The Challenge of Information Management within the Software Defined Vehicles
Tara Vatcher (Stellantis)
14:45
Using lightweight formal methods to check correctness of production code for Amazon S3
Rajeev Joshi (Amazon Web Services)
15:30
Abstract Interpretation of Floating-Point Digital Filters in Nuclear Plant Software
Pierre-Yves Piriou (EDF), Maxime Jacquemin (CEA) and Franck Védrine (CEA)
14:00
Chair: Corina Păsăreanu
Room: Sala 500
15:30
Industry Day
Chair: Nikolai Kosmatov
Room: Sala Madrid
15:30
Abstract Interpretation of Floating-Point Digital Filters in Nuclear Plant Software
Pierre-Yves Piriou (EDF), Maxime Jacquemin (CEA) and Franck Védrine (CEA)
15:30
Tool Demos (with Coffee Break)
Room: Expo Area
16:00
Coffee Break with Tool Demos
Room: Expo Area
ESOP: Types
Room: Sala Berlino
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: Sala 500
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: Sala Londra
16:30
Industry Day
Chair: Nikolai Kosmatov
Room: Sala Madrid
16:30
Advancing software solutions for CAR-T therapy manufacturing and standardization
Ethan Dhanraj (OmniaBio) and Hanene Ben Yedder (OmniaBio)
17:00
Agile Development: Ensuring Safety in Rapid Iteration Cycles
Mehrnoosh Askarpour (General Motors Canada), Sahar Kokaly (General Motors Canada) and Ramesh S (General Motors R&D)
17:30
Networking and informal discussions.
SPIN
Chair:
Room: Sala Parigi
16:30
19:00
ETAPS Banquet
Room: Giardino Delle Meraviglie