Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Tuesday 06 May
09:00
José Meseguer: Capturing System Designs with Formal Executable Specifications (FASE invited speaker)
Chair: Artur Boronat
Room: MDCL 1305
10:00
Coffee Break
Room: MDCL
TACAS: LTL
Chair: Sebastian Junges
Room: MDCL 1102
10:30
Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
Zili Wang, Katherine Kosaian and Kristin Yvonne Rozier
11:00
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning*
Jan Kretinsky, Tobias Meggendorfer, Maximilian Prokop and Ashkan Zarkhah
11:30
Learning real-time one-counter automata using polynomially many queries
Prince Mathew, Vincent Penelle and A V Sreejith
12:00
LydiaSyft: A Compositional Symbolic Synthesis Framework for LTLf Specifications
Shufang Zhu and Marco Favorito
12:15
Automating the Analysis of Quantitative Automata with QuAK
Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi and N. Ege Saraç
ESOP: Types
Chair: Viktor Vafeiadis
Room: MDCL 1305
10:30
Stratified Type Theory
Jonathan Chan and Stephanie Weirich
11:00
Elucidating Type Conversions in SQL Engines
Wenjia Ye, Matías Toro, Claudio Gutierrez, Bruno C. D. S. Oliveira and Éric Tanter
11:30
Named Arguments as Intersections, Optional Arguments as Unions
Yaozhu Sun and Bruno C. D. S. Oliveira
12:00
SMT-Boosted Security Types for Low-Level MPC
Christian Skalka and Joseph P. Near
FASE: MDE
Chair: Artur Boronat
Room: MDCL 1309
10:30
Compositional Learning for Synchronous Parallel Automata
Mahboubeh Samadi, Aryan Bastany and Hossein Hojjat
11:00
Symbolic State Partitioning for Reinforcement Learning*
Mohsen Ghaffari, Mahsa Varshosaz, Einar Broch Johnsen and Andrzej Wasowski
11:30
Formal Architectural Patterns for Adaptive Robotic Software
James Baxter, Bert van Acker, Morten Kristensen, Thomas Wright, Ana Cavalcanti and Cláudio Gomes
12:00
RoboScene: Notation for Formal Verification of Human-Robot Interaction
Holly Hendry, Ana Cavalcanti, Cade McCall and Mark Chattington
FOSSACS: Semantics
Chair: Petr Jančar
Room: MDCL 1105
10:30
Context-Free Languages of String Diagrams
Matt Earnshaw and Mario Román
11:00
Complete Test Suites for Automata in Monoidal Closed Categories
Bálint Kocsis and Jurriaan Rot
11:30
Idempotent Resources in Separation Logic
Daniel Gratzer, Mathias Adam Møller and Lars Birkedal
12:00
A Diagrammatic Algebra for Program Logics
Filippo Bonchi, Alessandro Di Giorgio and Elena Di Lavore
RUST WORKSHOP
Room: MDCL 1009
10:30
Using Rust and Verus for Development of Verified Operating Systems
Xiangdong Chen, Zhaofeng Li, Jerry Zhang and Anton Burtsev
11:00
VTock: Retrofitting automatic verification to a production microcontroller OS
Vivien Rindisbacher, Evan Johnson, Nico Lehmann, Ranjit Jhala and Deian Stefan
11:30
Vest: A Case Study of Verifying Performant, Higher-Order Rust Programs in Verus
Yi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya, Joshua Gancher, Milijana Surbatovich and Bryan Parno
12:00
Verification of Cryptographic Implementations in Lean with Aeneas
Son Ho, Aymeric Fromherz and Jonathan Protzenko
12:30
Lunch
Room: CIBC Hall & Foyer
TACAS: Verification I
Chair: Florian Zuleger
Room: MDCL 1102
14:00
Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs
Daniela Kaufmann and Jérémy Berthomieu
14:30
Cyclone: A Heterogeneous Tool for Verifying Infinite Descent*
Liron Cohen, Reuben Rowe and Matan Shaked
15:00
Implicit Rankings for Verifying Liveness Properties in First-Order Logic
Raz Lotan and Sharon Shoham
15:30
Neural Network Verification with Branch-and-Bound for General Nonlinearities
Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh and Huan Zhang
ESOP: Static Analysis
Chair: Ori Lahav
Room: MDCL 1305
14:00
Formal Verification of WTO-based Dataflow Solvers
Roméo La Spina, Delphine Demange and Sandrine Blazy
14:30
Efficient Synthesis of Tight Polynomial Upper-bounds for Systems of Conditional Polynomial Recurrences
Amir Goharshady, S. Hitarth and Sergei Novozhilov
15:00
Context-Sensitive Demand-Driven Control-Flow Analysis
Tim Whiting and Kimball Germane
15:30
Abstraction of memory block manipulations by symbolic loop folding
Jérôme Boillot and Jérôme Feret
FASE: Fundamentals
Chair: Mahsa Varshosaz
Room: MDCL 1309
14:00
Stochastic Timed Graph Transformation Systems
Sven Schneider, Maria Maximova and Holger Giese
14:30
Prove your Colorings: Formal Verification of Cache Coloring of Bao Hypervisor
Axel Ferréol, Laurent Corbin and Nikolai Kosmatov
15:00
Reasoning about Substitutability at the Level of Bytecode
Marco Paganoni and Carlo A. Furia
RUST WORKSHOP
Room: MDCL 1009
14:30
Verifying the Rust Standard Library
Carolyn Zech, Celina Val and Rahul Kumar
15:00
Initial Steps Toward Verifying the Rust Standard Library Using Verus
Elanor Tang, Travis Hance and Bryan Parno
15:30
Open Discussion
Ask-me-anything
Room: MDCL 1008
14:00
The Future of Conferences with Laura Kovacs and Marie Farrell
Host: Sebastian Junges
15:00
Software Liability, Legislation, AI Act, What Does It Mean For Us with Holger Hermanns and Tiziana Margaria
Host: Elizabeth Polgreen
16:00
Coffee Break
Room: MDCL
TACAS: SAT/SMT
Chair: Clark Barrett
Room: MDCL 1102
16:30
D-Painless: A Framework for Distributed Portfolio SAT Solving
Mazigh Saoudi, Souheib Baarir, Julien Sopena and Thibault Lejemble
17:00
Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation
David Chocholatý, Vojtěch Havlena, Lukáš Holík, Jan Hranička, Ondrej Lengal and Juraj Síč
17:30
Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation
Daimy Van Caudenberg, Bart Bogaerts and Leandro Vendramin
Arun Ross (Invited Tutorial)
Chair: Marieke Huisman
Room: MDCL 1305
RUST WORKSHOP
Room: MDCL 1009
16:30