Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Tuesday 06 May
09:00
10:00
Coffee Break
TACAS: LTL
Room:
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
Room:
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
Room:
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
Room:
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: None
Room:
10:30
12:30
Lunch
TACAS: Verification I
Room:
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
Room:
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
Room:
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: None
Room:
14:00
Ask-me-anything
Chair:
Room:
14:00
16:00
Coffee Break
TACAS: SAT/SMT
Room:
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:
Room:
RUST WORKSHOP: None
Room:
16:30