Programme
Programme of main conferences from Monday to Thursday.
Monday 13 April
08:45
ETAPS 2026 Opening
10:00
Coffee Break
TACAS: Proofs and Quantifier Elimination
Room:
10:30
Real-time Proof Checking for Distributed Incremental SAT Solving
Dominik Schreiber, Mathias Fleury, Katalin Fazekas and Armin Biere.
10:50
Enumerating Choice Terms in Model-Based Quantifier Instantiation
Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette and Cesare Tinelli.
11:10
Hint-Based SMT Proof Reconstruction
Joshua Clune, Haniel Barbosa and Jeremy Avigad.
11:30
Incremental Forward Reasoning for White-Box Proof Search
Xavier Généreux and Jannis Limperg.
11:50
QSOLE: Automatic QBF Equivalence Checking
Peter Pfeiffer, Mark Peyrer, Daniel Grosse and Martina Seidl.
12:00
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin and Georg Zetzsche.
12:10
Quantifier Elimination Meets Treewidth
Hao Wu, Jiyu Zhu, Amir Goharshady, Jie An, Bican Xia and Naijun Zhan.
FASE: SE and AI
Room:
10:30
Revisiting the Role of Natural Language Code Comments in Code Translation
Monika Gupta, Ajay Meena, Anamitra Roy Choudhury, Vijay Arya and Srikanta Bedathur.
10:50
From Words to Code: Do NLP Prompting Strategies Generalize to Code Generation?
Erin Woo, Sangyeop Yeo, Hyungkook Jun, Sangcheol Kim, Seung-won Hwang and Yu-Seung Ma.
11:10
LusGen: Leveraging LLMs for Safety-Critical Lustre Design and Requirements Traceability
Yili Jiang, Zhuoran Yan, Ning Ge, Yuan Wang, Jiahao Weng and Chunming Hu.
11:30
Quantifying Privacy Risks in Synthetic Data: A Study on Black-Box Membership Inference
Giacomo Fantino, Marco Rondina, Antonio Vetro' and Juan Carlos De Martin.
11:50
Formally correct search for interpretable DNFs
Imane Bousdira, Martin Cooper and Aurélie Hurault.
12:10
DivKC: A Divide-and-Conquer Approach to Knowledge Compilation
Olivier Zeyen, Karim Tit, Maxime Cordy and Gilles Perrouin.
FOSSACS: Logic, Model Checking, Formal Specifications
Room:
10:30
The Modal Logic of Abstraction Refinement
Jakob Piribauer and Vinzent Zschuppe.
10:50
Complete FSM Testing Using Strong Separability
Robert Hierons and Mohammad Reza Mousavi.
11:10
Synthesising Asynchronous Automata from Fair Specifications
Béatrice Bérard, Benjamin Monmege, B Srivathsan and Arnab Sur.
11:30
From Trees to Tree-Like: Distribution and Synthesis for Asynchronous Automata
Mathieu Lehaut, Anca Muscholl and Nir Piterman
11:50
Inquisitive team semantics of LTL
Laura Bozzelli, Tadeusz Litak, Munyque Mittelmann and Aniello Murano.
12:10
Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
Bernd Finkbeiner, Hadar Frenkel and Tim Rohde.
RUST
Chair:
Room:
10:30
12:30
Lunch Break
15:30
Tool Demos (with Coffee)
16:00
Coffee Break with Tool Demos
TACAS: Software Verification
Room:
16:30
Efficient Verification of Lingua Franca Programs
Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky, Mario Reja and Mikheil Rukhaia.
16:50
Verifying Floating-Point Programs in Stainless
Andrea Gilot, Axel Bergström and Eva Darulova.
17:10
A Case Study in Firmware Verification: Applying Formal Methods to Intel TDX Module
Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee and Thomas Lemberger.
17:30
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill and Clark Barrett.
17:50
When One Message Tells the Whole Story: Deciding Serializability in Network Systems
Guy Amir, Mark Barbone, Nicolas Amat and Jules Jacobs.
18:10
Extending FRET with SLEEC Rules: Formalization, Obligation Inference, and Monitoring
Mahrokh Mirani, Paola Inverardi, Patrizio Pelliccione, Franco Raimondi and Nicolas Troquard.
FASE: Advanced SW Development
Room:
16:30
Towards Decentralised Dynamic Reconfiguration of Software Systems
Mina Yavari and Damian Arellanes.
16:50
Analyses as First-Class Citizens in Model-Driven Development
Tianhai Liu, Shmuel Tyszberowicz and Bernhard Beckert.
17:10
Don’t go MAD with Anomalies! Design-time Microservice Anomaly Detection in Migration to Microservices
Valentim Romão, Rafael Soares, Luis Rodrigues and Vasco Manquinho.
17:30
EasyRPL - A web-based tool for modelling and analysis of cross-organisational workflows
Muhammad Rizwan Ali, Violet Ka I Pun and Guillermo Román-Díez.
17:50
ForumSeeker: Fusion Retrieval of Online Technical Forums for Effective Troubleshooting
Youyang Kim, Yaoping Ruan, Young-Kyoon Suh, Liqiang Wang and Byungchul Tak.
FOSSACS: Automata, Games, Concurrency Models
Room:
16:30
Well-quasi-orderings on word languages
Aliaume Lopez, Nathan Lhote and Lia Schuetze
16:50
The Complexity of Games with Randomised Control
Sarvin Bahmani, Rasmus Ibsen-Jensen, Soumyajit Paul, Sven Schewe, Friedrich Slivovsky, Qiyi Tang, Dominik Wojtczak and Shufang Zhu.
17:10
The Value Problem for Weighted Timed Games with Two Clocks is Undecidable
Isa Vialard, Joël Ouaknine and Quentin Guilmant.
17:30
Active Learning Techniques for Pomset Recognizers
Adrien Pommellet, Amazigh Amrane, Edgar Delaporte, Geoffroy Du Prey and Oscar Peyron.
17:50
On Reversibility in Petri Nets
Hernán Melgratti, Claudio Antares Mezzina and G. Michele Pinna.
18:10
Bridging the Gap Between Plain VASS and Branching VASS
Clotilde Bizière, Jérôme Leroux and Grégoire Sutre.
SV-Comp
Chair:
Room:
16:30
RUST
Chair:
Room:
16:30
19:00
ETAPS Reception
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
Wednesday 15 April
10:00
Coffee Break
TACAS: Automata
Room:
10:30
A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
Kyveli Doveri, Pierre Ganty and B Srivathsan.
10:50
Modular Attractor Acceleration in Infinite-State Games
Philippe Heim and Rayna Dimitrova.
11:10
Concurrent Permissive Strategy Templates
Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak and Anne-Kathrin Schmuck.
11:30
LTLf Learning Meets Boolean Set Cover
Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon and Pierre Vandenhove.
11:50
Faster Signature Refinement for Branching Bisimilarity Minimization
Jan J.M. Martens and Maurice Laveaux.
12:10
MightyPPL : Model Checking MITL with Past and Pnueli Modalities
Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya.
ESOP: Verification
Room:
10:30
Validating Quantum State Preparation Programs
Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett and Alex Potanin.
10:50
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Del Valle, Alexandra Silva and Marco Gaboardi.
11:10
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler.
11:30
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing
Philipp Schröer, Darion Haase and Joost-Pieter Katoen.
11:50
A Program Logic for Under-approximating Worst-case Resource Usage
Ziyue Jin and Di Wang.
12:10
Specification-Driven Generation of Summaries for Symbolic Execution
Rafael Gonçalves, Frederico Ramos, Pedro Adão and José Fragoso Santos.
FOSSACS: Lambda-Calculus, Program Semantics, Infinite Structures
Room:
10:30
Interaction Improvement
Adrienne Lancelot, Giulio Manzonetto, Guy McCusker and Gabriele Vanoni.
10:50
Lambda Galore
Mariangiola Dezani-Ciancaglini, Besik Dundua and Furio Honsell.
11:10
K Definitions as Matching Logic Theories, Formally
Xiaohong Chen, Horatiu Cheval, Dorel Lucanu and Grigore Rosu
11:30
Abstract Lipschitz Continuity: Combining Semantic and Quantitative Approximations
Marco Campion, Isabella Mastroeni, Michele Pasqua and Caterina Urban.
11:50
Composition Theorems for f-Differential Privacy
Annabelle McIver, Natasha Fernandes and Parastoo Sadeghi.
12:10
Karp's NP-complete problems over first-order definable structures
Aidan Healy and Bartek Klin.
SPIN
Chair:
Room:
10:30
Industry Day
Chair:
Room:
10:30
12:30
Lunch Break
13:00
ETAPS General Assembly
15:30
Tool Demos (with Coffee Break)
16:00
Coffee Break with Tool Demos
ESOP: Types
Room:
16:30
Lenses for Partially-Specified States
Kazutaka Matsuda, Minh Nguyen and Meng Wang.
16:50
In Cantor Space No One Can Hear You Stream
Martin Baillon, Assia Mahboubi and Pierre-Marie Pédrot.
17:10
Contextual Metaprogramming for Session Types
Pedro Ângelo, Atsushi Igarashi, Yuito Murase and Vasco T. Vasconcelos.
17:30
Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism
Patrycja Balik, Szymon Jędras and Piotr Polesiuk.
17:50
Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism
Hasti Toossi and Ningning Xie.
18:10
Auditing Rust Crates Effectively
Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan and Caleb Stanford.
18:20
Code Generation via Meta-programming in Dependently Typed Proof Assistants
Mathis Bouverot-Dupuis and Yannick Forster.
TACAS: Static Analysis & Program Verification
Room:
16:30
ReCheck: Automated Contextual Improvement Verifier for Functional Calculi across User-Defined Operational Semantics
Makoto Hamana and Kento Emoto
16:50
On Deciding Constant Runtime of Linear Loops
Florian Frohn, Jürgen Giesl, Peter Giesl and Nils Lommen.
17:10
Data Structure Analysis for Binaries
Sadra Bayat Tork, Nicholas Coughlin, Alicia Michael, James Tobler and Kirsten Winter
17:30
Integrating String Reasoning in Symbolic Execution of C Programs
Rachel Cleaveland and Clark Barrett.
17:50
Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Tree
Nat Karmios, Sacha-Elie Ayoun and Philippa Gardner.
18:10
Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities
Ali Rasim Kocal, Michael Schwarz, Simmo Saan and Helmut Seidl
AE Reports (30mins)
Chair:
Room:
16:30
Industry Day
Chair:
Room:
16:30
SPIN
Chair:
Room:
16:30
19:00
ETAPS Banquet
Thursday 16 April
10:00
Coffee Break
TACAS: CPS & Quantum
Room:
10:30
Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination
Lukas König, Christian Schildwächter, Michaela Klauck and Christian Heinzemann.
10:50
VeriLHyS: a Framework for LTL Specification and Verification of Hybrid Systems
Ludovico Battista, Stefano Tonetta and Gianni Zampedri.
11:10
TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics
S. Akshay, Prerak Contractor, Paul Gastin, R Govind and B Srivathsan.
11:30
Trace Repair Using Temporal Behavior Trees
Sebastian Schirmer, Philipp Schitz, Johann C. Dauer, Bernd Finkbeiner and Sriram Sankaranarayanan.
11:50
Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
Wei-Jia Huang, Jingyi Mei, Alfons Laarman, Yu-Fang Chen, Christophe Chareton, Kai-Min Chung and Min-Hsiu Hsieh.
12:10
Error-Tolerant Quantum State Discrimination: Optimization and Quantum Circuit Synthesis
Chien-Kai Ma, Bo-Hung Chen, Tian-Fu Chen, Dah-Wei Chiou and Jie-Hong Roland Jiang.
ESOP: Analysis
Room:
10:30
A Category-Theoretic Framework for Dependent Effect Systems
Satoshi Kura, Marco Gaboardi, Taro Sekiyama and Hiroshi Unno.
10:50
Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs
Han Xu and Di Wang.
11:10
Max-Policy Iteration, Revisited
David Monniaux and Helmut Seidl.
11:30
Complete Abstractions for Verification of Polymorphic Functions with Equality
Malo Revel, Thomas Genet and Thomas Jensen.
11:50
Modular Automatic Complexity Analysis of Recursive Integer Programs
Nils Lommen and Jürgen Giesl.
12:10
Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search
Yasmin Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh and Mahesh Viswanathan.
SPIN
Chair:
Room:
10:30
12:30
Lunch Break
TACAS: Model Checking & Hardware Verification
Room:
14:00
CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems
Roberto Pettinau and Christoph Matheja.
14:20
Verifying First-Order Temporal Properties of Infinite States Systems via Timers and Rankings
Raz Lotan, Neta Elad, Oded Padon and Sharon Shoham.
14:40
Revisiting Stateful Partial-Order Reduction
Frédéric Herbreteau, Gérald Point and Igor Walukiewicz.
15:00
Deconstructing Subset Construction: Reducing While Determinizing
Markus Frohme and John Nicol.
15:20
ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang and Cunxi Yu
15:40
EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
Guangyu Hu, Xiaofeng Zhou, Wei Zhang and Hongce Zhang.
Diversity, Equity, and Inclusion
Chair:
Room:
14:00
TEST-COMP
Chair:
Room:
14:00
SPIN
Chair:
Room:
14:00
16:00
Coffee Break
TACAS: SAT/SMT II
Room:
16:30
Parallel SMT Solving via Iterative Tree Partitioning
Tomáš Kolárik, Antti E.J. Hyvärinen, Seyedmasoud Asadzadeh and Natasha Sharygina.
16:50
Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob
Dominik Schreiber, Aina Niemetz and Mathias Preiner.
17:10
Exploring the SMT-LIB Benchmark Library
Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Pascal Fontaine, Cesare Tinelli and Clark Barrett.
17:30
SMT(LIA) Sampling with High Diversity
Yong Lai, Junjie Li and Chuan Luo.
17:50
BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability
Jakub Horák and Martin Jonáš.
18:10
SMTScope: Automated and Efficient Analysis of SMT Traces
Jonáš Fiala and Peter Müller.
SV-Comp and Test-Comp Community Building
Chair:
Room:
16:30
SPIN
Chair:
Room:
16:30
Accepted Papers
ESOP
moreless
- Guillaume Ambal, Max Stupple, Brijesh Dongol, Azalea Raad. Specifying and Verifying RDMA Synchronisation
- Pedro Ângelo, Atsushi Igarashi, Yuito Murase, Vasco T. Vasconcelos. Contextual Metaprogramming for Session Types
- Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot. In Cantor Space No One Can Hear You Stream
- Patrycja Balik, Szymon Jędras, Piotr Polesiuk. Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism
- Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao. Recursive Logical Relations for Intuitionistic Linear Logic Session Types
- Mathis Bouverot-Dupuis, Yannick Forster. Code Generation via Meta-programming in Dependently Typed Proof Assistants
- Sidney Congard, Guillaume Munch-Maccagnoni, Rémi Douence. Linear Effects, Exceptions, and Resource Safety
- John Derrick, Chelsea Edmonds, Andrei Popescu, Jamie Wright. Rely-Guarantee Is Coinductive: A Proof-Centered Investigation of Inductively Approximated Coinduction
- Namratha Reddy Gangamreddypalli, Constantin Enea, Shaz Qadeer. Reduction for Structured Concurrent Programs
- Rafael Gonçalves, Frederico Ramos, Pedro Adão, José Fragoso Santos. Specification-Driven Generation of Summaries for Symbolic Execution
- Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler. Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
- Ziyue Jin, Di Wang. A Program Logic for Under-approximating Worst-case Resource Usage
- Amir Karniel, Ori Lahav. Causal-Broadcast Memory
- Satoshi Kura, Marco Gaboardi, Taro Sekiyama, Hiroshi Unno. A Category-Theoretic Framework for Dependent Effect Systems
- Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett, Alex Potanin. Validating Quantum State Preparation Programs
- Xing Li, Yao Li, Peter Schachte, Christine Rizkallah. The Memorist Tale: Every Thunk Every Cost All At Once
- Nils Lommen, Jürgen Giesl. Modular Automatic Complexity Analysis of Recursive Integer Programs
- Kazutaka Matsuda, Minh Nguyen, Meng Wang. Lenses for Partially-Specified States
- Dylan McDermott, Nobuko Yoshida. Denotational reasoning for asynchronous multiparty session types
- David Monniaux, Helmut Seidl. Max-Policy Iteration, Revisited
- Duc Than Nguyen, William Mansky. A Formal Interface for Concurrent Search Structure Templates
- Malo Revel, Thomas Genet, Thomas Jensen. Complete Abstractions for Verification of Polymorphic Functions with Equality
- Yasmin Chandini Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh, Mahesh Viswanathan. Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search
- Philipp Schröer, Darion Haase, Joost-Pieter Katoen. Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing
- Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi. Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
- Hasti Toossi, Ningning Xie. Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism
- Toby Ueno, Ankush Das. Practical Refinement Session Type Inference
- Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Fu Song, Taolue Chen, David N. Jansen. A Formally Verified Procedure for Width Inference in FIRRTL
- Han Xu, Di Wang. Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs
- Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Santacruz Del Valle, Alexandra Silva, Marco Gaboardi. Outrunning Big KATs: Efficient Decision Procedure for Variants of GKAT
- Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan, Caleb Stanford. Auditing Rust Crates Effectively
FASE
moreless
- Mina Yavari and Damian Arellanes. Towards Decentralised Dynamic Reconfiguration of Software Systems
- Andrea Bombarda, Federico Conti, Marcello Minervini, Aurora Francesca Zanenga and Claudio Menghi. Failure Modes and Effects Analysis: An Experience from the E-Bike Domain
- Olivier Zeyen, Karim Tit, Maxime Cordy and Gilles Perrouin. DivKC: A Divide-and-Conquer Approach to Knowledge Compilation
- Giacomo Fantino, Marco Rondina, Antonio Vetro and Juan Carlos De Martin. Quantifying Privacy Risks in Synthetic Data: A Study on Black-Box Membership Inference
- Monika Gupta, Ajay Meena, Anamitra Roy Choudhury, Vijay Arya and Srikanta Bedathur. Revisiting the Role of Natural Language Code Comments in Code Translation
- Kaveh Aryan, Hana Chockler and Mohammad Reza Mousavi. Causal Liability in Autonomous Systems
- Tianhai Liu, Shmuel Tyszberowicz and Bernhard Beckert. Analyses as First-Class Citizens in Model-Driven Development
- Annalisa Sergi, Yousef Ahmed Abdel Rahman Shoeib, Andrea Bombarda, Nunzio Marco Bisceglia and Claudio Menghi. Search-based Software Testing for Drone Applications: An Experience with the Simulink Environment
- Imane Bousdira, Martin Cooper and Aurélie Hurault. Formally correct search for interpretable DNFs
- Valentim Romão, Rafael Soares, Luis Rodrigues and Vasco Manquinho. Don’t go MAD with Anomalies! Design-time Microservice Anomaly Detection in Migration to Microservices
- Aleksandar S. Dimovski. Abstract Symbolic Finite Automata for Algorithmic Game Semantics
- Erin Woo, Sangyeop Yeo, Hyungkook Jun, Sangcheol Kim, Seung-won Hwang and Yu-Seung Ma. From Words to Code: Do NLP Prompting Strategies Generalize to Code Generation?
- Muhammad Rizwan Ali, Violet Ka I Pun and Guillermo Román-Díez. EasyRPL - A web-based tool for modelling and analysis of cross-organisational workflows
- Bernhard Beckert, Andreas Bremer and Alexander Weigl. Timed Contract Automata
- Dóra Cziborová, Mihály Dobos-Kovács, Kristóf Marussy and András Vörös. Unified Timing-Aware Program Verification
- Youyang Kim, Yaoping Ruan, Young-Kyoon Suh, Liqiang Wang and Byungchul Tak. ForumSeeker: Fusion Retrieval of Online Technical Forums for Effective Troubleshooting
- Yili Jiang, Zhuoran Yan, Ning Ge, Yuan Wang, Jiahao Weng and Chunming Hu. LusGen: Leveraging LLMs for Safety-Critical Lustre Design and Requirements Traceability
- Mustafa Ghani and Holger Giese. Modeling and Analyzing Planning-Aware Distributed Cyber-Physical Systems with Timed Graph Transformation Systems
- Dirk Beyer, Thomas Lemberger and Henrik Wachowitz. Testing in Formal Verification via Witness Generation (Empirical Evaluation)
- Junjie Luo, Shangzhou Xia, Fuyuan Zhang and Jianjun Zhao. QEMI: A Quantum Software Stacks Testing Framework via Equivalence Module Inputs
- Artur Boronat. Composing Clinical Activity Guidance for Multimorbidity via Bounded Relational Analysis
FoSSaCS
moreless
- Paul Wild, Lutz Schröder, Karla Messing, Barbara König and Jonas Forster. Generalized Kantorovich-Rubinstein Duality beyond Hausdorff and Kantorovich
- Liam Chung and Tobias Kappé. Partial Reductions for Kleene Algebra with Single-Word Hypotheses
- Quentin Aristote and Daniela Petrisan. Learning bottom-up tree automata valued in monoidal categories
- Benjamin Plummer and Corina Cirstea. A Coalgebraic Approach to Infinite Games
- Aliaume Lopez, Nathan Lhote and Lia Schuetze. Well-quasi-orderings on word languages
- Jiri Adamek. Quantitative Algebras Presented via Monads
- Jakob Piribauer and Vinzent Zschuppe. The Modal Logic of Abstraction Refinement
- Matteo Spadetto. A 2-categorical approach to the semantics of dependent type theory with computation axioms
- Noé Delorme and Simon Perdrix. Diagrammatic Reasoning with Control as a Constructor, Applications to Quantum Circuits
- Marco Campion, Isabella Mastroeni, Michele Pasqua and Caterina Urban. Abstract Lipschitz Continuity: Combining Semantic and Quantitative Approximations
- Mariangiola Dezani-Ciancaglini, Besik Dundua and Furio Honsell. Lambda Galore
- Adrien Pommellet, Amazigh Amrane, Edgar Delaporte, Geoffroy Du Prey and Oscar Peyron. Active Learning Techniques for Pomset Recognizers
- Mayuko Kori and Kazuki Watanabe. A No-go Theorem for Coalgebraic Product Construction
- Aidan Healy and Bartek Klin. Karp’s NP-complete problems over first-order definable structures
- Xiaohong Chen, Horatiu Cheval, Dorel Lucanu and Grigore Rosu. K Definitions as Matching Logic Theories, Formally
- Laura Bozzelli, Tadeusz Litak, Munyque Mittelmann and Aniello Murano. Inquisitive team semantics of LTL
- Annabelle McIver, Natasha Fernandes and Parastoo Sadeghi. Composition Theorems for f-Differential Privacy
- Sarvin Bahmani, Rasmus Ibsen-Jensen, Soumyajit Paul, Sven Schewe, Friedrich Slivovsky, Qiyi Tang, Dominik Wojtczak and Shufang Zhu. The Complexity of Games with Randomised Control
- Robert Hierons and Mohammad Reza Mousavi. Complete FSM Testing Using Strong Separability
- Thea Li and Vladimir Zamdzhiev. Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach
- Isa Vialard, Joël Ouaknine and Quentin Guilmant. The Value Problem for Weighted Timed Games with Two Clocks is Undecidable
- Mathieu Lehaut, Anca Muscholl and Nir Piterman. From Trees to Tree-Like: Distribution and Synthesis for Asynchronous Automata
- Yoshiki Nakamura. A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead
- Adrienne Lancelot, Giulio Manzonetto, Guy McCusker and Gabriele Vanoni. Interaction Improvement
- Filippo Bonchi and Cipriano Junior Cioffo. Tapes as Stochastic Matrices of String Diagrams
- Hernán Melgratti, Claudio Antares Mezzina and G. Michele Pinna. On Reversibility in Petri Nets
- Yorgo Chamoun and Samuel Mimram. Realization of relational presheaves
- Béatrice Bérard, Benjamin Monmege, B Srivathsan and Arnab Sur. Synthesising Asynchronous Automata from Fair Specifications
- Bernd Finkbeiner, Hadar Frenkel and Tim Rohde. Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
- Clotilde Bizière, Jérôme Leroux and Grégoire Sutre. Bridging the Gap Between Plain VASS and Branching VASS
TACAS
moreless
- Julius Ide, Joost-Pieter Katoen, Hannah Mertens and Tim Quatmann. Multiple Long-Run and omega-Regular Objectives in MDPs
- Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel and Lev Nachmanson. Syntactically Convex Model-Based Projection for Linear Rational Arithmetic
- Angel He and David Parker. Robust Verification of Concurrent Stochastic Games
- Chia-Hsuan Lu, Tony Tan and Michael Benedikt. Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing
- Lukas König, Christian Schildwächter, Michaela Klauck and Christian Heinzemann. Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination
- Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang and Cunxi Yu. ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
- Charles Moloney, Robert Dyer and Elena Sherman. Demonstrating ARG-V’s Generation of Realistic Java Benchmarks for SV-COMP
- Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee and Thomas Lemberger. A Case Study in Firmware Verification: Applying Formal Methods to Intel TDX Module
- Ali Rasim Kocal, Michael Schwarz, Simmo Saan and Helmut Seidl. Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities
- Ludovico Battista, Stefano Tonetta and Gianni Zampedri. VeriLHyS: a Framework for LTL Specification and Verification of Hybrid Systems
- Xavier Généreux and Jannis Limperg. Incremental Forward Reasoning for White-Box Proof Search
- Tomáš Kolárik, Antti E.J. Hyvärinen, Seyedmasoud Asadzadeh and Natasha Sharygina. Parallel SMT Solving via Iterative Tree Partitioning
- Raz Lotan, Neta Elad, Oded Padon and Sharon Shoham. Verifying First-Order Temporal Properties of Infinite States Systems via Timers and Rankings
- Valentin Cassano, Pablo Castro, Raul Fervari and Pedro R. D’Argenio. AKR: A Model Checker for an Adaptative Probabilistic Knowing-How Logic
- Paolo Baldan, Sebastian Gurke, Barbara König and Florian Wittbold. Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games
- Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette and Cesare Tinelli. Enumerating Choice Terms in Model-Based Quantifier Instantiation
- Nat Karmios, Sacha-Elie Ayoun and Philippa Gardner. Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees
- 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. Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml
- Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin and Georg Zetzsche. Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
- Hao Wu, Jiyu Zhu, Amir Goharshady, Jie An, Bican Xia and Naijun Zhan. Quantifier Elimination Meets Treewidth
- Frédéric Herbreteau, Gérald Point and Igor Walukiewicz. Revisiting Stateful Partial-Order Reduction
- Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon and Pierre Vandenhove. LTLf Learning Meets Boolean Set Cover
- Jan J.M. Martens and Maurice Laveaux. Faster Signature Refinement for Branching Bisimilarity Minimization
- S. Akshay, Prerak Contractor, Paul Gastin, R Govind and B Srivathsan. TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics
- Dominik Schreiber, Aina Niemetz and Mathias Preiner. Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob
- Kyveli Doveri, Pierre Ganty and B Srivathsan. A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
- Sebastian Schirmer, Philipp Schitz, Johann C. Dauer, Bernd Finkbeiner and Sriram Sankaranarayanan. Trace Repair Using Temporal Behavior Trees
- Florian Frohn, Jürgen Giesl, Peter Giesl and Nils Lommen. On Deciding Constant Runtime of Linear Loops
- Rachel Cleaveland and Clark Barrett. Integrating String Reasoning in Symbolic Execution of C Programs
- Ka Lok Wu, Christa Jenkins, Scott Stoller and Omar Chowdhury. Automatically Tightening Access Control Policies with Restricter
- Joshua Clune, Haniel Barbosa and Jeremy Avigad. Hint-Based SMT Proof Reconstruction
- Guy Amir, Mark Barbone, Nicolas Amat and Jules Jacobs. When One Message Tells the Whole Story: Deciding Serializability in Network Systems
- Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Pascal Fontaine, Cesare Tinelli and Clark Barrett. Exploring the SMT-LIB Benchmark Library
- Wei-Jia Huang, Jingyi Mei, Alfons Laarman, Yu-Fang Chen, Christophe Chareton, Kai-Min Chung and Min-Hsiu Hsieh. Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
- Francesca Randone, Romina Doz, Mirco Tribastone and Luca Bortolussi. DeGAS: Gradient-Based Optimization of Probabilistic Programs without Sampling
- Yong Lai, Junjie Li and Chuan Luo. SMT(LIA) Sampling with High Diversity
- Mahrokh Mirani, Paola Inverardi, Patrizio Pelliccione, Franco Raimondi and Nicolas Troquard. Extending FRET with SLEEC Rules: Formalization, Obligation Inference, and Monitoring
- Sadra Bayat Tork, Nicholas Coughlin, Alicia Michael, James Tobler and Kirsten Winter. Data Structure Analysis for Binaries
- Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya. MightyPPL : Model Checking MITL with Past and Pnueli Modalities
- Jakub Horák and Martin Jonáš. BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability
- Philippe Heim and Rayna Dimitrova. Modular Attractor Acceleration in Infinite-State Games
- Markus Frohme and John Nicol. Deconstructing Subset Construction: Reducing While Determinizing
- Jonáš Fiala and Peter Müller. SMTScope: Automated and Efficient Analysis of SMT Traces
- Roberto Pettinau and Christoph Matheja. CTL-star Model Checking on Infinite Families of Finite-State Labeled Transition Systems
- Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky, Mario Reja and Mikheil Rukhaia. Efficient Verification of Lingua Franca Programs
- Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak and Anne-Kathrin Schmuck. Concurrent Permissive Strategy Templates
- Aina Niemetz and Mathias Preiner. Bit-Precise Interpolation in Bitwuzla
- Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill and Clark Barrett. VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
- Peter Pfeiffer, Mark Peyrer, Daniel Grosse and Martina Seidl. QSOLE: Automatic QBF Equivalence Checking
- Dominik Schreiber, Mathias Fleury, Katalin Fazekas and Armin Biere. Real-time Proof Checking for Distributed Incremental SAT Solving
- Andrea Gilot, Axel Bergström and Eva Darulova. Verifying Floating-Point Programs in Stainless
- Guangyu Hu, Xiaofeng Zhou, Wei Zhang and Hongce Zhang. EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
- Markus Anders, Cayden Codel and Marijn Heule. Orbitopal Fixing in SAT
- Lukas Panneke and Heike Wehrheim. jMT: Testing Correctness of Java Memory Models
- Chien-Kai Ma, Bo-Hung Chen, Tian-Fu Chen, Dah-Wei Chiou and Jie-Hong Roland Jiang. Error-Tolerant Quantum State Discrimination: Optimization and Quantum Circuit Synthesis
- Makoto Hamana and Kento Emoto. ReCheck: Automated Contextual Improvement Verifier for Functional Calculi across User-Defined Operational Semantics