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: Giorgio Audrito
Room: Sala Madrid
10:30
SPARK - Latest Industrial Challenges and Feature Development
Invited talk: Claire Dross (AdaCore)
11:10
Formal Methods at OCamlPro: SMT Solving with Alt-Ergo and Symbolic Execution with Owi
Hichem Rami Ait-El-Hara (OCamlPro)
11:30
Towards Sustainable Industrial Use of Formal Verification for Security Certification
Adel Djoudi (Thales) and Nikolai Kosmatov (Thales)
11:50
Semi-Formal Accuracy Analysis of an Industrial Path Computation Algorithm
Franck Vedrine (CEA List), Grégoire Boussu (Thales), Nikolai Kosmatov (Thales) and Bruno Lathuilière (EDF)
12:10
Precomputation: A New Era in Multi-Stage Programming
Seyed Hossein Haeri (Entropy Software Foundation)
12:30
Lunch Break
Room: Expo Area
13:00
ETAPS General Assembly
Room: Sala 500
Industry Day
Chair: Claire Dross
Room: Sala Madrid
14:00
Lean: A Unified Platform for Verification, Programming, and AI
Invited talk: Leonardo de Moura (AWS)
14:40
Check Adherence to Model in Modular and Distributed Cyber-Physical Production Systems
Abdelaziz Ouazzani Chahidi (Agnostic Production Systems), Hasnaa Ait Malek (Agnostic Production Systems), Maxime Morin (Agnostic Production Systems), Nicolas Navarro (Agnostic Production Systems), Darine Rammal (CEA List), Christophe Gaston (CEA List) and Arnault Lapitre (CEA List)
15:00
Semantics-Based Real-Time Verification for Web3
Grigore Rosu (Pi Squared), Dorel Lucanu (Pi Squared) and Xiaohong Chen (Pi Squared)
15:20
Industrial Orchestration of Testing Tools with SeaCoral
Nicolas Berthier (OCamlPro), Steven De Oliveira (OCamlPro), Nikolai Kosmatov (Thales) and Delphine Longuet (Thales)
15:40
On the Lookout for a “Bisimulation” Relation between Trace Sets for Early Design Evaluations
Gurvan Le Guernic (DGA)
Invited Tutorial
Chair: Corina Păsăreanu
Room: Sala 500
15:30
15:30: Tool Demos (with Coffee Break)
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
From Software Engineering to AI Engineering: Bridging the Research-Industry Gap in the Age of Intelligent Systems
Invited talk: Andrea Basso (Swiss Federal Institute of Technology, EPFL and Stanford University)
17:10
Toward a scalable methodology for Automating Safety Analysis
Stefano Minopoli (Collins Aerospace)
17:30
HPC4AI and Industry: Research Projects and Real-World Applications
Doriana Medic (Univ; of Turin) and Marco Aldinucci (Univ; of Turin)
SPIN
Chair:
Room: Sala Parigi
16:30
19:00
ETAPS Banquet
Room: Giardino Delle Meraviglie