Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Tuesday 14 April
10:00
Coffee Break
TACAS: Probabilistic Model Checking & Software Testing
Room:
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
AKR: A Model Checker for an Adaptative Probabilistic Knowing-How Logic
Valentin Cassano, Pablo Castro, Raul Fervari and Pedro R. D'Argenio.
12:00
Demonstrating ARG-V's Generation of Realistic Java Benchmarks for SV-COMP
Charles Moloney, Robert Dyer and Elena Sherman.
12:10
jMT: Testing Correctness of Java Memory Models
Lukas Panneke and Heike Wehrheim.
ESOP: Concurrency
Room:
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
Room:
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
Room:
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:
10:30
12:30
Lunch Break
14:00
Ask-Me-Anything Session
15:00
ETAPS Awards Talks
16:00
Coffee Break
TACAS: SAT/SMT I
Room:
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
Room:
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
Room:
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.
17:50
QEMI: A Quantum Software Stacks Testing Framework via Equivalence Module Inputs
Junjie Luo, Shangzhou Xia, Fuyuan Zhang and Jianjun Zhao.
FOSSACS: Category Theory, Coalgebra, Metric Systems
Room:
16:30
Quantitative Algebras Presented via 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:
16:30