TACAS: Model Checking
Chair: Kristin Rozier
Room: Hollenfels
14:00
JPF: From 2003 to 2023
Cyrille Valentin Artho, Pavel Parizek, Daohan Qu, Varadraj Galgali and Pu Yi
14:30
Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking
Muhammad Osama and Anton Wijs
15:00
Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
Lukas Koenig, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Kueperkoch, Dennis Fassbender and Michael Hanselmann
15:30
Enhancing GenMC's Usability and Performance
Michalis Kokologiannakis, Viktor Vafeiadis and Rupak Majumdar
ESOP: Effects and Modal Types
Chair: Kazutaka Matsuda
Room: Schengen II
14:00
Scoped Effects as Parameterized Algebraic Theories
Sam Lindley, Cristina Matache, Sean Moss, Sam Staton, Nicolas Wu and Zhixuan Yang
14:30
Monadic Intersection Types, Relationally*
Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni
15:00
Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis
Jason Z. S. Hu and Brigitte Pientka
15:30
Program Synthesis from Graded Types
Jack Hughes and Dominic Orchard
FoSSaCS: Categorical semantics
Chair: Corina Cirstea
Room: Diekirch-Echternach-Fischbach
14:00
Drawing from an Urn is Isometric
Bart Jacobs
14:30
Enriching Diagrams with Algebraic Operations
Alejandro Villoria, Henning Basold and Alfons Laarman
15:00
Monoidal Extended Stone Duality
Fabian Birkmann, Stefan Milius and Henning Urbat
15:30
Towards a Compositional Framework for Convex Analysis (with Applications to Probability Theory)
Dario Stein and Richard Samuelson
14:00
Invited talk: Next Generation Model-based Testing for Industrial Applications
Jan Peleska (Verified Systems International)
14:30
Invited talk: What Programmers Want from Proof with SPARK
Yannick Moy (AdaCore)
15:00
Retrospective on Formal Verification of a JavaCard Virtual Machine with Frama-C
Adel Djoudi (Thales Digital Identity & Security)
15:20
[15:20] Formal Methods in the Railways: Trajectory and Trends
Thierry Lecomte (Clearsy), Sébastien Agostini, David Déharbe, Julien Molinéro-Pérez, Erwan Mottin and Denis Sabatier
15:40
[15:40] Recommended Practice on Assurance of AI-enabled systems
Odd Ivar Haugen (DNV)
14:00
How to do modular verification of Rust programs using Kani – Tool Demo
Justus Adam, Felipe Monteiro and Celina Val
14:30
Concolic Execution for Mid-level Intermediate Representation of Rust Programs
Mohammad Omidvar Tehrani, Tan Khang Le, Frédéric Tuong and Steven Y. Ko
15:00
HACL-rs: A Verified Rust Cryptographic Library
Aymeric Fromherz, Jonathan Protzenko and Son Ho
15:30
Hax - Enabling High Assurance Cryptographic Software
Franziskus Kiefer, Karthikeyan Bhargavan, Lucas Franceschino, Lasse Letager Hansen, Jonas Schneider-Bensch and Bas Spitters
Ask-me-anything
Room: Europe A
14:00
On Ethics, AI and Programming with Tamar Sharon and Wolfgang Ahrendt
Host: Tom van Dijk
15:00
Putting Science on the Political Agenda with Ana Cavalcanti and Gerald Lüttgen
Host: Sebastian Junges