Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Monday 13 April
08:45
ETAPS 2026 Opening
Room: Sala 500
09:00
Christel Baier: Verification of Infinite-horizon Properties of Dynamic Bayesian Networks
Chair: Nathalie Bertrand
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: Proofs and Quantifier Elimination
Room: Sala 500
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: Sala Madrid
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: Sala Londra
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: Sala Parigi
10:30
12:30
Lunch Break
Room: Expo Area
14:00
Leonardo de Moura: The Lean Programming Language and Theorem Prover (Invited Tutorial)
Chair: Guy Katz
Room: Sala 500
15:30
Tool Demos (with Coffee)
Room: Expo Area
16:00
Coffee Break with Tool Demos
Room: Expo Area
TACAS: Software Verification
Room: Sala 500
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
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: Sala Madrid
16:30
QEMI: A Quantum Software Stacks Testing Framework via Equivalence Module Inputs
Junjie Luo, Shangzhou Xia, Fuyuan Zhang and Jianjun Zhao.
16:50
Towards Decentralised Dynamic Reconfiguration of Software Systems
Mina Yavari and Damian Arellanes.
17:10
Analyses as First-Class Citizens in Model-Driven Development
Tianhai Liu, Shmuel Tyszberowicz and Bernhard Beckert.
17:30
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:50
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.
18:10
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: Sala Londra
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: Sala Berlino
16:30
RUST
Chair:
Room: Sala Parigi
16:30
19:00
ETAPS Reception
Room: Corridoio Nizza
Tuesday 14 April
09:00
Einar Broch Johnsen: Formal Methods meet Digital Twins: Challenges and Opportunities
Chair: Robbert Krebbers
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: Probabilistic Model Checking & Software Testing
Room: Sala 500
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
jMT: Testing Correctness of Java Memory Models
Lukas Panneke and Heike Wehrheim.
12:10
Demonstrating ARG-V's Generation of Realistic Java Benchmarks for SV-COMP
Charles Moloney, Robert Dyer and Elena Sherman.
ESOP: Concurrency
Room: Sala Berlino
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: Sala Madrid
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: Sala Londra
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: Sala Parigi
10:30
12:30
Lunch Break
Room: Expo Area
14:00
Ask-Me-Anything Session
Chair: Sebastian Junges
Room: Sala 500
15:00
ETAPS Awards
Room: Sala 500
16:00
Coffee Break
Room: Expo Area
TACAS: SAT/SMT I
Room: Expo Area
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: Sala Berlino
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: Sala Madrid
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.
FOSSACS: Category Theory, Coalgebra, Metric Systems
Room: Sala Londra
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: Sala Parigi
16:30
Wednesday 15 April
09:00
Monika Henzinger: Guarding Privacy Over Time: Challenges and Solutions in Continuous Data Observation
Chair: Laura Kovács
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: Automata
Room: Expo Area
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: Sala Berlino
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: Sala Londra
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: Sala Parigi
10:30
Industry Day
Chair: Giorgio Audrito
Room: Sala Madrid
10:30
SPARK - Latest Industrial Challenges and Feature Development
Invited talk: Claire Dross (AdaCore)
11:10
Formal Methods at OCamlPro: SMT Solving with Alt-Ergo and Symbolic Execution with Owi
Hichem Rami Ait-El-Hara (OCamlPro)
11:30
Towards Sustainable Industrial Use of Formal Verification for Security Certification
Adel Djoudi (Thales) and Nikolai Kosmatov (Thales)
11:50
Semi-Formal Accuracy Analysis of an Industrial Path Computation Algorithm
Franck Vedrine (CEA List), Grégoire Boussu (Thales), Nikolai Kosmatov (Thales) and Bruno Lathuilière (EDF)
12:10
Precomputation: A New Era in Multi-Stage Programming
Seyed Hossein Haeri (Entropy Software Foundation)
12:30
Lunch Break
Room: Expo Area
13:00
ETAPS General Assembly
Room: Sala 500
Industry Day
Chair: Claire Dross
Room: Sala Madrid
14:00
Lean: A Unified Platform for Verification, Programming, and AI
Invited talk: Leonardo de Moura (AWS)
14:40
Check Adherence to Model in Modular and Distributed Cyber-Physical Production Systems
Abdelaziz Ouazzani Chahidi (Agnostic Production Systems), Hasnaa Ait Malek (Agnostic Production Systems), Maxime Morin (Agnostic Production Systems), Nicolas Navarro (Agnostic Production Systems), Darine Rammal (CEA List), Christophe Gaston (CEA List) and Arnault Lapitre (CEA List)
15:00
Semantics-Based Real-Time Verification for Web3
Grigore Rosu (Pi Squared), Dorel Lucanu (Pi Squared) and Xiaohong Chen (Pi Squared)
15:20
Industrial Orchestration of Testing Tools with SeaCoral
Nicolas Berthier (OCamlPro), Steven De Oliveira (OCamlPro), Nikolai Kosmatov (Thales) and Delphine Longuet (Thales)
15:40
On the Lookout for a “Bisimulation” Relation between Trace Sets for Early Design Evaluations
Gurvan Le Guernic (DGA)
Invited Tutorial
Chair: Corina Păsăreanu
Room: Sala 500
15:30
15:30: Tool Demos (with Coffee Break)
16:00
Coffee Break with Tool Demos
Room: Expo Area
ESOP: Types
Room: Sala Berlino
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: Sala 500
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: Sala Londra
16:30
Industry Day
Chair: Nikolai Kosmatov
Room: Sala Madrid
16:30
From Software Engineering to AI Engineering: Bridging the Research-Industry Gap in the Age of Intelligent Systems
Invited talk: Andrea Basso (Swiss Federal Institute of Technology, EPFL and Stanford University)
17:10
Toward a scalable methodology for Automating Safety Analysis
Stefano Minopoli (Collins Aerospace)
17:30
HPC4AI and Industry: Research Projects and Real-World Applications
Doriana Medic (Univ; of Turin) and Marco Aldinucci (Univ; of Turin)
SPIN
Chair:
Room: Sala Parigi
16:30
19:00
ETAPS Banquet
Room: Giardino Delle Meraviglie
Thursday 16 April
09:00
Guy Van Den Broeck: Symbolic Reasoning in the Age of Large Language Models
Chair: Sebastian Junges
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: CPS & Quantum
Room: Sala 500
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: Sala Berlino
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: Sala Parigi
10:30
12:30
Lunch Break
Room: Expo Area
TACAS: Model Checking & Hardware Verification
Room: Sala 500
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.
16:00
AKR: A Model Checker for an Adaptative Probabilistic Knowing-How Logic
Valentin Cassano, Pablo Castro, Raul Fervari and Pedro R. D'Argenio.
Diversity, Equity, and Inclusion
Chair: Maurice ter Beek and Ferruccio Damiani
Room: Sala Londra
14:00
TEST-COMP
Chair:
Room: Sala Madrid
14:00
SPIN
Chair:
Room: Sala Parigi
14:00
16:00
Coffee Break
Room: Expo Area
TACAS: SAT/SMT II
Room: Sala 500
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: Sala Madrid
16:30
SPIN
Chair:
Room: Sala Parigi
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. 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