Log in | Join us

Programme

Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.

Weekend Monday Tuesday Wednesday Thursday
Download program in PDF

Tuesday 14 April

09:00
Einar Broch Johnsen: Formal Methods meet Digital Twins: Challenges and Opportunities
Chair: Robbert Krebbers
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: Probabilistic Model Checking & Software Testing
Chair: Matthias Volk
Room: Sala 500
10:30
Multiple Long-Run and omega-Regular Objectives in MDPs
Julius Ide, Joost-Pieter Katoen, Hannah Mertens and Tim Quatmann.
10:50
Robust Verification of Concurrent Stochastic Games
Angel He and David Parker.
11:10
Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games
Paolo Baldan, Sebastian Gurke, Barbara König and Florian Wittbold.
11:30
DeGAS: Gradient-Based Optimization of Probabilistic Programs without Sampling
Francesca Randone, Romina Doz, Mirco Tribastone and Luca Bortolussi.
11:50
jMT: Testing Correctness of Java Memory Models
Lukas Panneke and Heike Wehrheim.
12:10
Demonstrating ARG-V's Generation of Realistic Java Benchmarks for SV-COMP
Charles Moloney, Robert Dyer and Elena Sherman.
ESOP: Concurrency
Chair: Robbert Krebbers
Room: Sala Berlino
10:30
Denotational reasoning for asynchronous multiparty session types
Dylan McDermott and Nobuko Yoshida.
10:50
Practical Refinement Session Type Inference
Toby Ueno and Ankush Das.
11:10
Recursive Logical Relations for Intuitionistic Linear Logic Session Types*
Stephanie Balzer, Farzaneh Derakhshan, Robert Harper and Yue Yao.
11:30
A Formal Interface for Concurrent Search Structure Templates
Duc Than Nguyen and William Mansky.
11:50
Reduction for Structured Concurrent Programs
Namratha Gangamreddypalli, Constantin Enea and Shaz Qadeer.
12:10
Rely-Guarantee Is Coinductive: A Proof-Centered Investigation of Inductively Approximated Coinduction
John Derrick, Chelsea Edmonds, Andrei Popescu and Jamie Wright.
FASE: Autonomous Systems/Applications
Chair: Luigia Petre
Room: Sala Parigi
10:30
Failure Modes and Effects Analysis: An Experience from the E-Bike Domain
Andrea Bombarda, Federico Conti, Marcello Minervini, Aurora Francesca Zanenga and Claudio Menghi.
10:50
Causal Liability in Autonomous Systems
Kaveh Aryan, Hana Chockler and Mohammad Reza Mousavi.
11:10
Search-based Software Testing for Drone Applications: An Experience with the Simulink Environment
Annalisa Sergi, Yousef Ahmed Abdel Rahman Shoeib, Andrea Bombarda, Nunzio Marco Bisceglia and Claudio Menghi.
11:30
Modeling and Analyzing Planning-Aware Distributed Cyber-Physical Systems with Timed Graph Transformation Systems
Mustafa Ghani and Holger Giese.
11:50
Composing Clinical Activity Guidance for Multimorbidity via Bounded Relational Analysis
Artur Boronat.
FOSSACS: Kleene Algebra, Expressions, String Diagrams, Categorical Logic
Chair: Igor Walukiewicz
Room: Sala Londra
10:30
Partial Reductions for Kleene Algebra with Single-Word Hypotheses
Liam Chung and Tobias Kappé.
10:50
A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead
Yoshiki Nakamura.
11:10
Tapes as Stochastic Matrices of String Diagrams
Filippo Bonchi and Cipriano Junior Cioffo.
11:30
Diagrammatic Reasoning with Control as a Constructor, Applications to Quantum Circuits
Noé Delorme and Simon Perdrix.
11:50
Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach
Thea Li and Vladimir Zamdzhiev.
12:10
Realization of relational presheaves
Yorgo Chamoun and Samuel Mimram.
RUST
Chair:
Room: Sala Madrid
10:30
Verifying the Rust standard library with Creusot
Li-Yao Xia, Arnaud Golfouse and Jacques-Henri Jourdan
11:00
Extending Verus with Logical Atomicity
Aaron Bies
11:30
Supporting Weak Memory in Verus
Natalie Neamtu, Elanor Tang, Laila Elbeheiry, Hoang-Hai Dang, Derek Dreyer, Travis Hance, Chris Hawblitzel and Bryan Parno
12:00
Foundationally Verifying Real-World Rust Programs
Lennard Gäher and Vincent Lafeychine
12:30
Lunch Break
Room: Expo Area
ETAPS Awards and Ask-Me-Anything Session
Room: Sala 500
14:00
Ask-Me-Anything Session
Chair: Sebastian Junges
15:00
ETAPS Awards
Chair: Laura Kovács
RUST
Chair:
Room: Sala Madrid
14:00
Charon: An Analysis Framework for Rust
Guillaume Boisseau, Son Ho and Aymeric Fromherz
14:20
Verifying curve25519-dalek in Verus
Lacramioara Astefanoaei, Sergiu Bursuc, Jure Kukovec, Theodore Ehrenborg, Shaowei Lin and Max Tegmark
14:40
Verifying curve25519-dalek in Lean
Oliver Butterley, Markus Dablander, Alessandro D’Angelo, Hoang Le Truong, Liao Zhang
15:00
HiRustVer: Verifying Industrial Rust Code in Practice – An Ongoing Case Study
Guanyan Li and Haokun Li
15:30
KMIR Meets Real World Rust: An Experience Report
Daniel Cumming
16:00
Coffee Break
Room: Expo Area
TACAS: SAT/SMT I
Chair: Guy Amir
Room: Sala 500
16:30
Syntactically Convex Model-Based Projection for Linear Rational Arithmetic
Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel and Lev Nachmanson.
16:50
Bit-Precise Interpolation in Bitwuzla
Aina Niemetz and Mathias Preiner.
17:10
Orbitopal Fixing in SAT*
Markus Anders, Cayden Codel and Marijn Heule.
17:30
Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml
João Madeira Pereira, Filipe Marques, Pedro Adão, Hichem Rami Ait-El-Hara, Léo Andrès, Arthur Carcano, Pierre Chambart, Petar Maksimović, Nuno Santos and José Fragoso Santos.
17:50
Automatically Tightening Access Control Policies with Restricter
Ka Lok Wu, Christa Jenkins, Scott Stoller and Omar Chowdhury.
18:10
Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing
Chia-Hsuan Lu, Tony Tan and Michael Benedikt.
ESOP: Semantics & Compilation
Chair: Nobuko Yoshida
Room: Sala Berlino
16:30
Causal-Broadcast Memory
Amir Karniel and Ori Lahav.
16:50
Specifying and Verifying RDMA Synchronisation
Guillaume Ambal, Max Stupple, Brijesh Dongol and Azalea Raad.
17:10
A Formally Verified Procedure for Width Inference in FIRRTL
Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Taolve Chen, Fu Song and David N. Jansen.
17:30
Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki and Naoki Kobayashi.
17:50
Linear Effects, Exceptions, and Resource Safety: A Curry-Howard Correspondence for Destructors
Sidney Congard, Guillaume Munch-Maccagnoni and Rémi Douence.
18:10
The Memorist Tale: Every Thunk Every Cost All At Once
Xing Li, Yao Li, Peter Schachte and Christine Rizkallah.
FASE: Testing and Verification
Chair: Dirk Beyer
Room: Sala Parigi
16:30
Abstract Symbolic Finite Automata for Algorithmic Game Semantics
Aleksandar S. Dimovski.
16:50
Timed Contract Automata
Bernhard Beckert, Andreas Bremer and Alexander Weigl.
17:10
Unified Timing-Aware Program Verification
Dóra Cziborová, Mihály Dobos-Kovács, Kristóf Marussy and András Vörös.
17:30
Testing in Formal Verification via Witness Generation (Empirical Evaluation)
Dirk Beyer, Thomas Lemberger and Henrik Wachowitz.
FOSSACS: Category Theory, Coalgebra, Metric Systems
Chair: Stefan Milius
Room: Sala Londra
16:30
Varieties of Quantitative Algebras Presented by 1-Basic Monads
Jiri Adamek.
16:50
Generalized Kantorovich-Rubinstein Duality beyond Hausdorff and Kantorovich
Paul Wild, Lutz Schröder, Karla Messing, Barbara König and Jonas Forster.
17:10
Learning bottom-up tree automata valued in monoidal categories*
Quentin Aristote and Daniela Petrisan.
17:30
A Coalgebraic Approach to Infinite Games
Benjamin Plummer and Corina Cirstea.
17:50
A No-go Theorem for Coalgebraic Product Construction
Mayuko Kori and Kazuki Watanabe.
18:10
A 2-categorical approach to the semantics of dependent type theory with computation axioms
Matteo Spadetto.
RUST
Chair:
Room: Sala Madrid
16:30
A Program Logic for Tree Borrows
Johannes Hostert and Ralf Jung
17:00
Corten: Foundational Verification for Rust via Separation Logic
Frantisek Farka, Carmine Abate, Sebastian Ertel, Andrei Listochkin and Sven Linker
17:30
RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
Jinhua Wu, Yuting Wang, Liukun Yu and Linglong Meng
Programme in PDF for print
Full Programme

ETAPS Association

Internal

Responsible for these web pages:

Jan Kofroň
Faculty of Mathematics and Physics
Charles University, Czech Republic
E-mail: firstname.lastname [at] d3s.mff.cuni.cz
Phone: +420 951 554 285