|
08:45
|
Opening
Room: Europe A
|
|
09:00
|
Lars Birkedal: Higher-Order Probabilistic Relational Separation Logic (unifying speaker)
Room: Europe A
Chair: Ana Cavalcanti
|
|
10:00
|
Coffee break
Room: Europe C
|
|
10:30
11:00
11:15
11:30
12:00
|
TACAS: SAT and SMT
Chair: Laura Kovács
Room: Hollenfels
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike and John Backes
Z3-Noodler: An Automata-based String Solver
Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč
TaSSAT: Transferring and Sharing in SAT
Md Solimul Chowdhury, Cayden Codel and Marijn Heule
Speculative SAT modulo SAT
Hari Govind Vediramana Krishnan, Isabel Garcia-Contreras, Sharon Shoham and Arie Gurfinkel
Happy ending: An empty hexagon in every set of 30 points
Marijn Heule and Manfred Scheucher
|
TACAS: Synthesis
Chair: Bernd Finkbeiner
Room: Diekirch-Echternach-Fischbach
Fully Generalized Reactivity(1) Synthesis
Rüdiger Ehlers and Ayrat Khalimov
Knor: reactive synthesis using Oink
Tom van Dijk, Feije van Abbema and Naum Tomov
On Dependent Variables in Reactive Synthesis
S. Akshay, Eliyahu Basa, Dror Fried and Supratik Chakraborty
CESAR: Control Envelope Synthesis via Angelic Refinements
Aditi Kabra, Jonathan Laurent, Stefan Mitsch and André Platzer
|
FASE: Runtime Approaches
Chair: Reiner Hähnle
Room: Schengen II
Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models
Lucas Sakizloglou, Holger Giese, and Leen Lambers
Probabilistic Runtime Enforcement of Executable BPMN Processes
Yliès Falcone, Gwen Salaün, and Ahang Zuo
Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems
He Xu, Sven Schneider, and Holger Giese
Formal Specification of Trusted Execution Environment APIs
Geunyeol Yu, Seunghyun Chae, Kyungmin Bae, and Sungkun Moon
|
Rust
Room: Schengen I
Tree Borrows
Neven Villani, Johannes Hostert, Ralf Jung and Derek Dreyer
Aeneas: Rust Verification by Functional Translation
Son Ho, Jonathan Protzenko and Aymeric Fromherz
Contracts for Rust
Felix Klock and Celina Val
Building User-Friendly Rust Verification Tools
Federico Poli
|
|
12:30
|
Lunch
Room: Europe B
|
|
14:00
14:30
14:45
15:00
15:30
|
TACAS: Proof Checking
Chair: Marijn Heule
Room: Hollenfels
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
Hanna Lachnitt, Cesare Tinelli, Andrew Reynolds, Andres Noetzli, Haniel Barbosa, Leni Aniva, Clark Barrett and Mathias Fleury
Automate where Automation Fails: Proof Strategies for Frama-C/WP
Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov
VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification
Mertcan Temel
A State-of-the-Art Karp-Miller Algorithm Certified in Coq
Thibault Hilaire, David Ilcinkas and Jérôme Leroux
A Logical Treatment of Finite Automata
Nishant Rodrigues, Mircea Sebe, Xiaohong Chen and Grigore Rosu
|
FASE: System Comprehension
Chair: Andrzej Wąsowski
Room: Schengen II
Monitoring the Future of Smart Contracts
Margarita Capretto, Martin Ceresa, and Cesar Sanchez
Comprehending Object State via Dynamic Class Invariant Learning
Jan H. Boockmann, and Gerald Luettgen
Smart Issue Detection for Large-Scale Online Service Systems Using Multi-Channel Data
Liushan Chen, Yu Pei, Mingyang Wan, Zhihui Fei, Tao Liang, and Guojun Ma
Refinement Verification of OS Services based on a Verified Preemptive Microkernel
Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang, and Zhiping Shi
|
Rust
Room: Schengen I
Verifiying a Concurrent Memory Allocator with Verus
Travis Hance
Efficiently Verifying Rust Traits with SMT Solvers
Chris Hawblitzel
OxiDD: Verification Challenge
Nils Husung, Clemens Dubslaff and Maximilian Alexander Köhl
Rust Verification Workshop Proposal: Crowdsourcing the Rust standard library verification
Celina G. Val and Rahul Kumar
|
Competition of Software Verification (SV-COMP)
Chair: Dirk Beyer
Room: Diekirch-Echternach-Fischbach
Introduction to SV-COMP
Dirk Beyer
Bubaak (Marek Chalupa), Bubaak-SpLit (Cedric Richter), ConcurrentWitness2Test (Levente Bajczi), CPAchecker (Daniel Baier), CPV (Po-Chun Chien)
EmergenTheta (Zsófia Ádám), ESBMC (Rafael Sá Menezes), Goblint (Michael Schwarz), Goblint Validator (Simmo Saan)
Korn (Gidon Ernst), LIV (Marian Lingsch-Rosenfeld), Mopsa (Raphaël Monat), PredatorHP (Veronika Šoková), PROTON (Ravindra Metta), SWAT (Nils Loose), Symbiotic (Jan Strejček), Theta (Csanád Telbisz)
UAutomizer (Matthias Heizmann), UGemCutter (Dominik Klumpp), UKojak (Frank Schüssele), VeriAbsL (Priyanka Darke), Witch 3 (Paulína Ayaziová), WitnessLint (Marian Lingsch-Rosenfeld)
|
Diversity & Inclusion
Chair: Peter Roenne
Room: Europe A
Why do we talk about Equality and Diversity in research?
Inês Crisóstomo
The Computer Girls: Exploring Herstory
Valérie Schafer
Building an Inclusive Researcher Journey
Véronique Schlick
Interactive session and discussion
|
|
16:00
|
Coffee break
Room: Europe C
|
|
16:30
17:00
17:30
|
TACAS: Logic and Decidability
Chair: Sebastian Junges
Room: Hollenfels
Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains
Lukas Westhofen, Christian Neurohr, Daniel Neider and Jean Christoph Jung
Deciding Boolean Separation Logic via Small Models
Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar and Florian Zuleger
Asynchronous Subtyping by Trace Relaxation
Laura Bocchi, Andy King and Maurizio Murgia
|
Invited Tutorial
Chair: Marieke Huisman
Room: Europe A
David Monniaux: Flavors of Abstract Interpretation
|
Rust
Room: Schengen I
Panel Discussion / Lightning Talks
|
Competition of Software Verification (SV-COMP)
Chair: Dirk Beyer
Room: Diekirch-Echternach-Fischbach
Open SV-COMP Community Meeting
|
|
09:00
|
Sandrine Blazy: From Operational Semantics to Verified Compilation (unifying speaker)
Room: Europe A
Chair: Stephanie Weirich
|
|
10:00
|
Coffee Break
Room: Europe C
|
|
10:30
11:00
11:30
11:45
12:00
12:15
|
FASE: Fuzzing and NIER
Chair: Dirk Beyer
Room: Schengen II
Fuzzy quantitative attack tree analysis
Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg, and Mariëlle Stoelinga
Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation
Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura, Vasco Manquinho, and Ruben Martins
Invariant-based Program Repair
Omar Al-Bataineh
Can ChatGPT support software verification?
Cedric Richter and Heike Wehrheim
Combining Deductive Verification with Shape Analysis
Téo Bernier, Yani Ziani, Nikolai Kosmatov, and Frédéric Loulergue
First Steps towards Deductive Verification of LLVM IR
Dré van Oorschot, Marieke Huisman, and Ömer Şakar
|
TACAS: Program Analysis and Proofs
Chair: Andrei Voronkov
Room: Hollenfels
SootUp: A Redesign of the Soot Static Analysis Framework
Kadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo and Dongjie He
Formally verified asymptotic consensus in robust networks
Mohit Tekriwal, Avi-Tachna Fram, Jean-Baptiste Jeannin, Manos Kapritsos and Dimitra Panagou
Formally Verifying an Efficient Sorter
Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler and Sascha Witt
Explainable Online Monitoring of Metric First-Order Temporal Logic
Leonardo Lima, Jonathan Huerta Y Munive and Dmitriy Traytel
|
FoSSaCS: Infinite games
Chair: Shaull Almagor
Room: Diekirch-Echternach-Fischbach
Fair Omega-regular Games
Daniel Hausmann, Nir Piterman, Irmak Saglam and Anne-Kathrin Schmuck
Stochastic Window Mean-payoff Games
Laurent Doyen, Pranshu Gaba and Shibashis Guha
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
Daniel Hausmann, Mathieu Lehaut and Nir Piterman
Parity Games on Temporal Graphs
Pete Austin, Sougata Bose and Patrick Totzke
|
Industry Day
Room: Wiltz
Invited talk: Formal Verification of Avionics Software
David Delmas (Airbus Operations SAS)
Collision-Free Trajectories in Automated Driving: Extending a Formal Argumentation From Single Scenarios to Scenario Ranges
Franziska Henze (CARIAD SE)
[11:20] How Bosch Brings Formal Methods to Autonomous Systems Engineering
Michaela Klauck (Robert Bosch GmbH), Christian Heinzemann and Ralph Lange
[11:40] Invited talk: European R&D Projects: Participation and Opportunities
Leonardo Tonetto (Advisor ‑ European R&D and Innovation Support)
[12:15] Networking Session
Each participant can present a 1-minute no-slide pitch about their interests in collaboration
|
Rust
Room: Schengen I
A hybrid approach to semi-automated Rust verification
Xavier Denis and Sacha-Elie Ayoun
Advances in the Rust compiler to ease the development of verification tools
Celina G. Val and Oli Scherer
Towards sound journeys through unsafe areas riding VeriFast
Nima Rahimi Foroushaani and Bart Jacobs
Refinement Proofs in Rust using Ghost Locks
Aurel Bílý
|
|
12:30
|
Lunch
Room: Europe B
|
|
14:00
14:30
15:00
15:30
|
TACAS: Model Checking
Chair: Kristin Rozier
Room: Hollenfels
JPF: From 2003 to 2023
Cyrille Valentin Artho, Pavel Parizek, Daohan Qu, Varadraj Galgali and Pu Yi
Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking
Muhammad Osama and Anton Wijs
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
Enhancing GenMC's Usability and Performance
Michalis Kokologiannakis, Viktor Vafeiadis and Rupak Majumdar
|
ESOP: Effects and Modal Types
Chair: Kazutaka Matsuda
Room: Schengen II
Scoped Effects as Parameterized Algebraic Theories
Sam Lindley, Cristina Matache, Sean Moss, Sam Staton, Nicolas Wu and Zhixuan Yang
Monadic Intersection Types, Relationally
Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni
Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis
Jason Z. S. Hu and Brigitte Pientka
Program Synthesis from Graded Types
Jack Hughes and Dominic Orchard
|
FoSSaCS: Categorical semantics
Chair: Corina Cirstea
Room: Diekirch-Echternach-Fischbach
Drawing from an Urn is Isometric
Bart Jacobs
Enriching Diagrams with Algebraic Operations
Alejandro Villoria, Henning Basold and Alfons Laarman
Monoidal Extended Stone Duality
Fabian Birkmann, Stefan Milius and Henning Urbat
Towards a Compositional Framework for Convex Analysis (with Applications to Probability Theory)
Dario Stein and Richard Samuelson
|
Industry Day
Room: Wiltz
Invited talk: Next Generation Model-based Testing for Industrial Applications
Jan Peleska (Verified Systems International)
Invited talk: What Programmers Want from Proof with SPARK
Yannick Moy (AdaCore)
Retrospective on Formal Verification of a JavaCard Virtual Machine with Frama-C
Adel Djoudi (Thales Digital Identity & Security)
[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] Recommended Practice on Assurance of AI-enabled systems
Odd Ivar Haugen (DNV)
|
Rust
Room: Schengen I
How to do modular verification of Rust programs using Kani – Tool Demo
Justus Adam, Felipe Monteiro and Celina Val
Concolic Execution for Mid-level Intermediate Representation of Rust Programs
Mohammad Omidvar Tehrani, Tan Khang Le, Frédéric Tuong and Steven Y. Ko
HACL-rs: A Verified Rust Cryptographic Library
Aymeric Fromherz, Jonathan Protzenko and Son Ho
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
On Ethics, AI and Programming with Tamar Sharon and Wolfgang Ahrendt
Host: Tom van Dijk
Putting Science on the Political Agenda with Ana Cavalcanti and Gerald Lüttgen
Host: Sebastian Junges
|
|
16:00
|
Coffee break
Room: Europe C
|
|
16:30
17:00
17:30
|
TACAS: Automata and Learning
Chair: Anne-Kathrin Schmuck
Room: Hollenfels
Scalable Tree-based Register Automata Learning
Paul Fiterau-Brostean, Simon Dierl, Falk Howar, Bengt Jonsson, Konstantinos Sagonas and Fredrik Tåquist
Small Test Suites for Active Automata Learning
Loes Kruger, Sebastian Junges and Jurriaan Rot
Mata: A Fast and Simple Finite Automata Library
David Chocholatý, Tomas Fiedor, Vojtěch Havlena, Lukáš Holík, Martin Hruska, Ondrej Lengal and Juraj Síč
|
Invited Tutorial
Chair: Lenore Zuck
Room: Europe A
Tamar Sharon: The view from ethics: What technologies promise, what they do and who benefits
|
Industry Day
Room: Wiltz
Invited talk: From Theory to Practice: What is a contract, really?
Fritz Henglein (Deon Digital)
Formal Methods in Web3: Success Stories and Opportunities
Franck Cassez (Mantle Research)
[17:20] Securing the Aptos Framework through formal verification with the Move Prover
Wolfgang Grieskamp (Aptos Labs), Junkil Park and Teng Zhang
[17:40] Experience Report: Formally Verifying Critical Blockchain Network Component
Bhargav Bhatt (Web3 Foundation)
|
Rust
Room: Schengen I
Panel Discussion
|
|
09:00
|
Jérôme Leroux: The Petri Net Reachability Problem (FoSSaCS invited speaker)
Room: Europe A
Chair: Naoki Kobayashi
|
|
10:00
|
Coffee Break
Room: Europe C
|
|
10:30
11:00
11:30
12:00
|
TACAS: Software Verification
Chair: Tomáš Vojnar
Room: Hollenfels
Accelerated Bounded Model Checking Using Interpolation Based Summaries
Mayank Solanki, Prantik Chatterjee, Akash Lal and Subhajit Roy
Weakest Precondition Inference for Non-Deterministic Linear Array Programs
Sumanth Prabhu, Deepak D'Souza, Supratik Chakraborty, Venkatesh R and Grigory Fedyukovich
Automated Software Verification of Hyperliveness
Raven Beutner
A Comprehensive Specification and Verification of the L4 Microkernel API
Leping Zhang, Yongwang Zhao and Jianxin Li
|
ESOP: Domain-Specific Languages
Chair: Josh Ko
Room: Schengen II
Circuit Width Estimation via Effect Typing and Linear Dependency
Andrea Colledan and Ugo Dal Lago
Reconciling Partial and Local Invertibility
Anders Ågren Thuné, Kazutaka Matsuda and Meng Wang
On the Hardness of Analyzing Quantum Programs Quantitatively
Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix
Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping
Hiroya Fujinami and Ichiro Hasuo
|
FoSSaCS: Automata and Synthesis
Chair: Bart Jacobs
Room: Diekirch-Echternach-Fischbach
Determinization of Integral Discounted-Sum Automata is Decidable
Shaull Almagor and Neta Dafni
Checking History-Determinism is NP-hard for Parity Automata
Aditya Prakash
Tighter Construction of Tight Büchi Automata
Marek Jankola and Jan Strejček
Synthesis with Privacy Against an Observer
Orna Kupferman, Ofer Leshkowitz and Naama Shamash Halevy
|
Spin: Software Verification
Chair: Thomas Neele
Room: Schengen I
Taming the AI Monster: Monitoring of Individual Fairness for Effective Human Oversight (keynote)
Holger Hermanns
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants
Dirk Beyer, Po-Chun Chien and Nian-Ze Lee
Test-Case Generation with Automata-based Software Model Checking
Max Barth and Marie-Christine Jakobs
|
|
12:30
|
Lunch
Room: Europe B
|
|
13:00
|
ETAPS General Assembly
Room: Europe A
|
|
14:00
14:30
15:00
15:30
|
TACAS: Probabilistic Systems
Chair: Kim Larsen
Room: Hollenfels
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler
CTMCs with Imprecisely Timed Observations
Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga and Nils Jansen
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot and Sebastian Junges
Learning Explainable and Better Performing Representations of POMDP Strategies
Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky and Stefanie Mohr
|
ESOP: Bidirectional typing / Session types
Chair: Ugo Dal Lago
Room: Schengen II
A formal treatment of bidirectional typing
Liang-Ting Chen and Hsiang-Shang Ko
Generic bidirectional typing for dependent type theories
Thiago Felicissimo
The Session Abstract Machine
Luis Caires and Bernardo Toninho
Deciding Subtyping for Asynchronous Multiparty Sessions
Elaine Li, Felix Stutz and Thomas Wies
|
FoSSaCS: Types and Programming Languages
Chair: James Worrell
Room: Diekirch-Echternach-Fischbach
From Rewrite Rules to Axioms in the lambdaPi-Calculus Modulo Theory
Valentin Blot, Gilles Dowek, Thomas Traversié and Théo Winterhalter
Light Genericity
Beniamino Accattoli and Adrienne Lancelot
Logical Predicates in Higher-Order Mathematical Operational Semantics
Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas and Henning Urbat
On Basic Feasible Functionals and the Interpretation Method
Patrick Baillot, Ugo Dal Lago, Cynthia Kop and Deivid Vale
|
Spin: Anniversary Track
Chair: Anton Wijs
Room: Schengen I
The Spin on Spin (keynote)
Gerald Holzmann
Two Decades of Industrializing Formal Verification: The Reactis Story
Rance Cleaveland, David Hansel, Steve Sims and Scott Smolka
Automated Reasoning in Quantum Circuit Compilation
Dimitrios Thanos, Alejandro Villoria, Sebastiaan Brand, Arend-Jan Quist, Jingyi Mei, Tim Coopmans and Alfons Laarman
|
Tool demo session
Room: Europe B
|
|
16:00
|
Coffee break
Room: Europe C
|
|
16:30
17:00
17:30
|
TACAS: Simulations
Chair: Javier Esparza
Room: Hollenfels
Dissipative quadratizations of polynomial ODE systems
Yubo Cai and Gleb Pogudin
Forward and Backward Constrained Bisimulations for Quantum Circuits
Antonio Jiménez-Pastor, Kim Guldstrand Larsen, Mirco Tribastone and Max Tschaikowski
A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation
Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán and Yon Shin Teo
|
ESOP: Dependent Types
Chair: Benoit Montagu
Room: Schengen II
Observational Equality Meets CIC
Loïc Pujet and Nicolas Tabareau
Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance and Assia Mahboubi
Definitional Functoriality for Dependent (Sub)Types
Théo Laurent, Meven Lennon-Bertrand and Kenji Maillard
|
TACAS: Neural Networks
Chair: Arie Gurfinkel
Room: Diekirch-Echternach-Fischbach
Provable Preimage Under-Approximation for Neural Networks
Xiyue Zhang, Benjie Wang and Marta Kwiatkowska
Training for Verification: Increasing Neuron Stability to Scale DNN Verification
Dong Xu, Nusrat Jahan Mozumder, Hai Duong and Matthew Dwyer
NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis
Matthias Cosler, Christopher Hahn, Ayham Omar and Frederik Schmitt
|
Spin: Automated Reasoning
Chair: Alfons Laarman
Room: Schengen I
Random Access on Narrow Decision Diagrams in External Memory
Steffan Christ Sølvsten, Casper Moldrup Rysgaard and Jaco van de Pol
Solving Constrained Horn Clauses as C Programs with CHC2C
Levente Bajczi and Vince Molnár
|
|
09:00
|
Ruzica Piskac (TACAS invited speaker)
Room: Europe A
Chair: Laura Kovacs
|
|
10:00
|
Coffee Break
Room: Europe C
|
|
10:30
11:00
11:30
12:00
|
TACAS: Testing and Verification
Chair: Ruzica Piskac
Room: Hollenfels
HaliVer: Deductive Verification and Scheduling Languages Join Forces
Lars B. van den Haak, Anton Wijs, Marieke Huisman and Mark van den Brand
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage
Martin Jonáš, Jan Strejček, Marek Trtík and Lukáš Urban
Fast Symbolic Computation of Bottom SCCs
Anna Blume Jakobsen, Rasmus Skibdahl Melanchton Jorgensen, Andreas Pavlogiannis and Jaco van de Pol
Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers
Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee and Nils Sirrenberg
|
ESOP: Verification and Analysis
Chair: Ori Lahav
Room: Schengen II
Verified Inlining and Specialisation for PureCake
Hrutvik Kanabar, Kacper Korban and Magnus O. Myreen
Maximal Quantified Precondition Synthesis for Linear Array Loops
Sumanth Prabhu, Grigory Fedyukovich and Deepak D'Souza
Higher-Order LCTRSs and Their Termination
Liye Guo and Cynthia Kop
Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
Daniel Lundén, Lars Hummelgren, Jan Kudlicka, Oscar Eriksson and David Broman
|
FoSSaCS: Logic and Proofs
Chair: Ichiro Hasuo
Room: Diekirch-Echternach-Fischbach
Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems
Luca Geatti, Alessio Mansutti and Angelo Montanari
A Resolution-Based Interactive Proof System for UNSAT
Philipp Czerner, Javier Esparza and Valentin Krasotin
Craig Interpolation for Decidable First-Order Fragments
Balder ten Cate and Jesse Comer
Clones, closed categories, and combinatory logic
Philip Saville
|
Spin: Verification Tools
Chair: Matthias Heizmann
Room: Schengen I
Learning the State Machine Behind a Modal Text Editor: The (Neo)Vim Case Study
Pierre Ganty
Tolerange: Quantifying Fault Masking in Stochastic Systems
Luciano Putruele, Ramiro Demasi, Pablo Castro and Pedro D'Argenio
Software Verification Witnesses 2.0
Paulína Ayaziová, Dirk Beyer, Marian Lingsch-Rosenfeld, Martin Spiessl and Jan Strejček
Fault Localization on Verification Witnesses
Dirk Beyer, Matthias Kettl and Thomas Lemberger
|
|
12:30
|
Lunch
Room: Europe B
|
|
14:00
14:30
15:00
15:30
|
TACAS: Games
Chair: Bernd Finkbeiner
Room: Hollenfels
Auction-Based Scheduling
Guy Avni, Kaushik Mallik and Suman Sadhukhan
Most General Winning Secure Equilibria Synthesis in Graph Games
Satya Prakash Nayak and Anne-Kathrin Schmuck
On-The-Fly Algorithm for Reachability in Parametric Timed Games
Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci and Jaco van de Pol
Rabin Games and Colourful Universal Trees
Rupak Majumdar, Irmak Saglam and K. S. Thejaswini
|
ESOP: Verification
Chair: Luis Caires
Room: Schengen II
A Denotational Approach to Release-Acquire Concurrency
Yotam Dvir, Ohad Kammar and Ori Lahav
Specifying and Verifying Persistent Libraries
Léo Stefanesco, Azalea Raad and Viktor Vafeiadis
Intel PMDK Transactions: Specification and Concurrency
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer and Brijesh Dongol
Hyperproperty Verification as CHC Satisfiability
Shachar Itzhaky, Sharon Shoham and Yakir Vizel
|
FoSSaCS: Infinite-State Systems
Chair:: Jerome Leroux
Room: Diekirch-Echternach-Fischbach
Reachability in Fixed VASS: Expressiveness and Lower Bounds
Andrei Draghici, Christoph Haase and Andrew Ryzhikov
From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
Jan-Christoph Kassing, Florian Frohn and Jürgen Giesl
Dimension-Minimality and Primality of Counter Nets
Shaull Almagor, Guy Avni, Henry Sinclair-Banks and Asaf Yeshurun
Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
Lucie Guillou, Corto Mascle and Nicolas Waldburger
|
Spin: Model Checking
Chair: Anton Wijs
Room: Ansembourg
MoXI: An Intermediate Language for Symbolic Model Checking (keynote)
Kristin Yvonne Rozier
Synchronisation in Language-level Symmetry Reduction for Probabilistic Model Checking
Ivaylo Valkov, Alastair Donaldson and Alice Miller
A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method
Daisuke Ishii
|
Award Winner Presentations
Chair: Marieke Huisman
Room: Europe A
Doctoral Dissertation Award
Yotam Feldman: Towards a Theory of Learning Inductive Invariants
Test Of Time Award
Luca Cardelli and Andrew D. Gordon: Mobile Ambients
Test-Of-Time Tool Award
Marta Kwiatkowska, Gethin Norman, and David Parker: PRISM
Artifact Evaluation Report & Awards
Arnd Hartmanns, Hadar Frenkel, and Tobias Kappé
|
|
16:00
|
Coffee break
Room: Europe C
|
|
16:30
17:00
17:30
|
TACAS: Concurrency
Chair: Hadar Frenkel
Room: Hollenfels
Verification under TSO with an infinite Data Domain
Florian Furbach, Parosh Aziz Abdulla, Mohamed Faouzi Atig and Shashwat Garg
OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust
Nils Husung, Clemens Dubslaff, Holger Hermanns and Maximilian Alexander Köhl
Decidable Verification under Localized Release-Acquire Concurrency
Abhishek Kr Singh and Ori Lahav
|
ESOP: Abstract Interpretation
Chair: Thomas Wies
Room: Schengen II
A Modular Soundness Theory for the Blackboard Analysis Architecture
Sven Keidel, Dominik Helm, Tobias Roth and Mira Mezini
Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
Raphaël Monat, Aymeric Fromherz and Denis Merigoux
Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation
Pierre Lermusiaux and Benoit Montagu
|
Competition on Software Testing (Test-Comp)
Chair: Dirk Beyer
Room: Schengen I
Introduction to Test-Comp
Dirk Beyer
CoVeriTest (Marie-Christine Jakobs), ESBMC (Rafael Sá Menezes), FuSeBMC (Rafael Sá Menezes), Fizzer (Lukáš Urban), Utestgen (Max Barth)
Discussion
|