|
08:45
|
ETAPS 2026 Opening
Room: Sala 500
|
|
09:00
|
Christel Baier: Verification of Infinite-horizon Properties of Dynamic Bayesian Networks
Room: Sala 500
Chair: Nathalie Bertrand
|
|
10:00
|
Coffee Break
Room: Expo Area
|
|
10:30
10:50
11:10
11:30
11:50
12:00
12:10
|
TACAS: Proofs and Quantifier Elimination
Room: Sala 500
Real-time Proof Checking for Distributed Incremental SAT Solving
Dominik Schreiber, Mathias Fleury, Katalin Fazekas and Armin Biere.
Enumerating Choice Terms in Model-Based Quantifier Instantiation
Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette and Cesare Tinelli.
Hint-Based SMT Proof Reconstruction
Joshua Clune, Haniel Barbosa and Jeremy Avigad.
Incremental Forward Reasoning for White-Box Proof Search
Xavier Généreux and Jannis Limperg.
QSOLE: Automatic QBF Equivalence Checking
Peter Pfeiffer, Mark Peyrer, Daniel Grosse and Martina Seidl.
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin and Georg Zetzsche.
Quantifier Elimination Meets Treewidth
Hao Wu, Jiyu Zhu, Amir Goharshady, Jie An, Bican Xia and Naijun Zhan.
|
FASE: SE and AI
Chair: Elvira Albert and Corina Pasareanu
Room: Sala Madrid
Revisiting the Role of Natural Language Code Comments in Code Translation
Monika Gupta, Ajay Meena, Anamitra Roy Choudhury, Vijay Arya and Srikanta Bedathur.
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.
LusGen: Leveraging LLMs for Safety-Critical Lustre Design and Requirements Traceability
Yili Jiang, Zhuoran Yan, Ning Ge, Yuan Wang, Jiahao Weng and Chunming Hu.
Quantifying Privacy Risks in Synthetic Data: A Study on Black-Box Membership Inference
Giacomo Fantino, Marco Rondina, Antonio Vetro' and Juan Carlos De Martin.
Formally correct search for interpretable DNFs
Imane Bousdira, Martin Cooper and Aurélie Hurault.
DivKC: A Divide-and-Conquer Approach to Knowledge Compilation
Olivier Zeyen, Karim Tit, Maxime Cordy and Gilles Perrouin.
|
FOSSACS: Logic, Model Checking, Formal Specifications
Chair: Joost-Pieter Katoen
Room: Sala Londra
The Modal Logic of Abstraction Refinement
Jakob Piribauer and Vinzent Zschuppe.
Complete FSM Testing Using Strong Separability
Robert Hierons and Mohammad Reza Mousavi.
Synthesising Asynchronous Automata from Fair Specifications
Béatrice Bérard, Benjamin Monmege, B Srivathsan and Arnab Sur.
From Trees to Tree-Like: Distribution and Synthesis for Asynchronous Automata
Mathieu Lehaut, Anca Muscholl and Nir Piterman
Inquisitive team semantics of LTL
Laura Bozzelli, Tadeusz Litak, Munyque Mittelmann and Aniello Murano.
Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
Bernd Finkbeiner, Hadar Frenkel and Tim Rohde.
|
FM4All
Chair: Luigia Petre
Room: Sala Berlino
|
RUST
Chair:
Room: Sala Parigi
|
|
12:30
|
Lunch Break
Room: Expo Area
|
|
14:00
|
Leonardo de Moura: The Lean Programming Language and Theorem Prover (Invited Tutorial)
Room: Sala 500
Chair: Guy Katz
|
|
15:30
|
Tool Demos and Posters (with Coffee)
Room: Expo Area
|
|
16:00
|
Coffee Break with Tool Demos and Posters
Room: Expo Area
|
|
16:30
16:50
17:10
17:30
17:50
18:10
|
TACAS: Software Verification
Room: Sala 500
Efficient Verification of Lingua Franca Programs
Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky, Mario Reja and Mikheil Rukhaia.
Verifying Floating-Point Programs in Stainless
Andrea Gilot, Axel Bergström and Eva Darulova.
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.
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.
Deciding Serializability in Network Systems
Guy Amir, Mark Barbone, Nicolas Amat and Jules Jacobs.
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
Chair: Artur Boronat
Room: Sala Madrid
QEMI: A Quantum Software Stacks Testing Framework via Equivalence Module Inputs
Junjie Luo, Shangzhou Xia, Fuyuan Zhang and Jianjun Zhao.
Towards Decentralised Dynamic Reconfiguration of Software Systems
Mina Yavari and Damian Arellanes.
Analyses as First-Class Citizens in Model-Driven Development
Tianhai Liu, Shmuel Tyszberowicz and Bernhard Beckert.
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.
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.
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
Chair: B. Srivathsan
Room: Sala Londra
Well-quasi-orderings on word languages
Aliaume Lopez, Nathan Lhote and Lia Schuetze
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.
The Value Problem for Weighted Timed Games with Two Clocks is Undecidable
Isa Vialard, Joël Ouaknine and Quentin Guilmant.
Active Learning Techniques for Pomset Recognizers
Adrien Pommellet, Amazigh Amrane, Edgar Delaporte, Geoffroy Du Prey and Oscar Peyron.
On Reversibility in Petri Nets
Hernán Melgratti, Claudio Antares Mezzina and G. Michele Pinna.
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
|
RUST
Chair:
Room: Sala Parigi
|
|
19:00
|
ETAPS Reception
Room: Corridoio Nizza
|
|
09:00
|
Einar Broch Johnsen: Formal Methods meet Digital Twins: Challenges and Opportunities
Room: Sala 500
Chair: Robbert Krebbers
|
|
10:00
|
Coffee Break
Room: Expo Area
|
|
10:30
10:50
11:10
11:30
11:50
12:10
|
TACAS: Probabilistic Model Checking & Software Testing
Room: Sala 500
Multiple Long-Run and omega-Regular Objectives in MDPs
Julius Ide, Joost-Pieter Katoen, Hannah Mertens and Tim Quatmann.
Robust Verification of Concurrent Stochastic Games
Angel He and David Parker.
Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games
Paolo Baldan, Sebastian Gurke, Barbara König and Florian Wittbold.
DeGAS: Gradient-Based Optimization of Probabilistic Programs without Sampling
Francesca Randone, Romina Doz, Mirco Tribastone and Luca Bortolussi.
jMT: Testing Correctness of Java Memory Models
Lukas Panneke and Heike Wehrheim.
Demonstrating ARG-V's Generation of Realistic Java Benchmarks for SV-COMP
Charles Moloney, Robert Dyer and Elena Sherman.
|
ESOP: Concurrency
Room: Sala Berlino
Denotational reasoning for asynchronous multiparty session types
Dylan McDermott and Nobuko Yoshida.
Practical Refinement Session Type Inference
Toby Ueno and Ankush Das.
Recursive Logical Relations for Intuitionistic Linear Logic Session Types
Stephanie Balzer, Farzaneh Derakhshan, Robert Harper and Yue Yao.
A Formal Interface for Concurrent Search Structure Templates
Duc Than Nguyen and William Mansky.
Reduction for Structured Concurrent Programs
Namratha Gangamreddypalli, Constantin Enea and Shaz Qadeer.
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
Chair: Luigia Petre
Room: Sala Madrid
Failure Modes and Effects Analysis: An Experience from the E-Bike Domain
Andrea Bombarda, Federico Conti, Marcello Minervini, Aurora Francesca Zanenga and Claudio Menghi.
Causal Liability in Autonomous Systems
Kaveh Aryan, Hana Chockler and Mohammad Reza Mousavi.
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.
Modeling and Analyzing Planning-Aware Distributed Cyber-Physical Systems with Timed Graph Transformation Systems
Mustafa Ghani and Holger Giese.
Composing Clinical Activity Guidance for Multimorbidity via Bounded Relational Analysis
Artur Boronat.
|
FOSSACS: Kleene Algebra, Expressions, String Diagrams, Categorical Logic
Chair: Igor Walukiewicz
Room: Sala Londra
Partial Reductions for Kleene Algebra with Single-Word Hypotheses
Liam Chung and Tobias Kappé.
A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead
Yoshiki Nakamura.
Tapes as Stochastic Matrices of String Diagrams
Filippo Bonchi and Cipriano Junior Cioffo.
Diagrammatic Reasoning with Control as a Constructor, Applications to Quantum Circuits
Noé Delorme and Simon Perdrix.
Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach
Thea Li and Vladimir Zamdzhiev.
Realization of relational presheaves
Yorgo Chamoun and Samuel Mimram.
|
RUST
Chair:
Room: Sala Parigi
|
|
12:30
|
Lunch Break
Room: Expo Area
|
|
14:00
|
Ask-Me-Anything Session
Room: Sala 500
Chair: Sebastian Junges
|
|
15:00
|
ETAPS Awards
Room: Sala 500
|
|
16:00
|
Coffee Break
Room: Expo Area
|
|
16:30
16:50
17:10
17:30
17:50
18:10
|
TACAS: SAT/SMT I
Room: Expo Area
Syntactically Convex Model-Based Projection for Linear Rational Arithmetic
Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel and Lev Nachmanson.
Bit-Precise Interpolation in Bitwuzla
Aina Niemetz and Mathias Preiner.
Orbitopal Fixing in SAT
Markus Anders, Cayden Codel and Marijn Heule.
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.
Automatically Tightening Access Control Policies with Restricter
Ka Lok Wu, Christa Jenkins, Scott Stoller and Omar Chowdhury.
Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing
Chia-Hsuan Lu, Tony Tan and Michael Benedikt.
|
ESOP: Semantics & Compilation
Room: Sala Berlino
Causal-Broadcast Memory
Amir Karniel and Ori Lahav.
Specifying and Verifying RDMA Synchronisation
Guillaume Ambal, Max Stupple, Brijesh Dongol and Azalea Raad.
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.
Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki and Naoki Kobayashi.
Linear Effects, Exceptions, and Resource Safety: A Curry-Howard Correspondence for Destructors
Sidney Congard, Guillaume Munch-Maccagnoni and Rémi Douence.
The Memorist Tale: Every Thunk Every Cost All At Once
Xing Li, Yao Li, Peter Schachte and Christine Rizkallah.
|
FASE: Testing and Verification
Chair: Dirk Beyer
Room: Sala Madrid
Abstract Symbolic Finite Automata for Algorithmic Game Semantics
Aleksandar S. Dimovski.
Timed Contract Automata
Bernhard Beckert, Andreas Bremer and Alexander Weigl.
Unified Timing-Aware Program Verification
Dóra Cziborová, Mihály Dobos-Kovács, Kristóf Marussy and András Vörös.
Testing in Formal Verification via Witness Generation (Empirical Evaluation)
Dirk Beyer, Thomas Lemberger and Henrik Wachowitz.
|
FOSSACS: Category Theory, Coalgebra, Metric Systems
Chair: Stefan Milius
Room: Sala Londra
Quantitative Algebras Presented via Monads
Jiri Adamek.
Generalized Kantorovich-Rubinstein Duality beyond Hausdorff and Kantorovich
Paul Wild, Lutz Schröder, Karla Messing, Barbara König and Jonas Forster.
Learning bottom-up tree automata valued in monoidal categories
Quentin Aristote and Daniela Petrisan.
A Coalgebraic Approach to Infinite Games
Benjamin Plummer and Corina Cirstea.
A No-go Theorem for Coalgebraic Product Construction
Mayuko Kori and Kazuki Watanabe.
A 2-categorical approach to the semantics of dependent type theory with computation axioms
Matteo Spadetto.
|
RUST
Chair:
Room: Sala Parigi
|
|
09:00
|
Monika Henzinger: Guarding Privacy Over Time: Challenges and Solutions in Continuous Data Observation
Room: Sala 500
Chair: Laura Kovács
|
|
10:00
|
Coffee Break
Room: Expo Area
|
|
10:30
10:50
11:10
11:30
11:50
12:10
|
TACAS: Automata
Room: Expo Area
A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
Kyveli Doveri, Pierre Ganty and B Srivathsan.
Modular Attractor Acceleration in Infinite-State Games
Philippe Heim and Rayna Dimitrova.
Concurrent Permissive Strategy Templates
Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak and Anne-Kathrin Schmuck.
LTLf Learning Meets Boolean Set Cover
Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon and Pierre Vandenhove.
Faster Signature Refinement for Branching Bisimilarity Minimization
Jan J.M. Martens and Maurice Laveaux.
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
Validating Quantum State Preparation Programs
Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett and Alex Potanin.
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Del Valle, Alexandra Silva and Marco Gaboardi.
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.
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing
Philipp Schröer, Darion Haase and Joost-Pieter Katoen.
A Program Logic for Under-approximating Worst-case Resource Usage
Ziyue Jin and Di Wang.
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
Chair: Barbara König
Room: Sala Londra
Interaction Improvement
Adrienne Lancelot, Giulio Manzonetto, Guy McCusker and Gabriele Vanoni.
Lambda Galore
Mariangiola Dezani-Ciancaglini, Besik Dundua and Furio Honsell.
K Definitions as Matching Logic Theories, Formally
Xiaohong Chen, Horatiu Cheval, Dorel Lucanu and Grigore Rosu
Abstract Lipschitz Continuity: Combining Semantic and Quantitative Approximations
Marco Campion, Isabella Mastroeni, Michele Pasqua and Caterina Urban.
Composition Theorems for f-Differential Privacy
Annabelle McIver, Natasha Fernandes and Parastoo Sadeghi.
Karp's NP-complete problems over first-order definable structures
Aidan Healy and Bartek Klin.
|
SPIN
Chair:
Room: Sala Parigi
|
Industry Day
Chair: Giorgio Audrito
Room: Sala Madrid
SPARK - Latest Industrial Challenges and Feature Development
Invited talk: Claire Dross (AdaCore)
Formal Methods at OCamlPro: SMT Solving with Alt-Ergo and Symbolic Execution with Owi
Hichem Rami Ait-El-Hara (OCamlPro)
Towards Sustainable Industrial Use of Formal Verification for Security Certification
Adel Djoudi (Thales) and Nikolai Kosmatov (Thales)
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)
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
|
|
14:00
14:40
15:00
15:20
15:40
|
Industry Day
Chair: Claire Dross
Room: Sala Madrid
Lean: A Unified Platform for Verification, Programming, and AI
Invited talk: Leonardo de Moura (AWS)
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)
Semantics-Based Real-Time Verification for Web3
Grigore Rosu (Pi Squared), Dorel Lucanu (Pi Squared) and Xiaohong Chen (Pi Squared)
Industrial Orchestration of Testing Tools with SeaCoral
Nicolas Berthier (OCamlPro), Steven De Oliveira (OCamlPro), Nikolai Kosmatov (Thales) and Delphine Longuet (Thales)
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
Mieke Massink: Model Checking in Space with Applications to Medical Image Analysis
15:30: Tool Demos and Posters (with Coffee Break)
|
|
16:00
|
Coffee Break with Tool Demos and Posters
Room: Expo Area
|
|
16:30
16:50
17:10
17:30
17:50
18:10
18:20
|
ESOP: Types
Room: Sala Berlino
Lenses for Partially-Specified States
Kazutaka Matsuda, Minh Nguyen and Meng Wang.
In Cantor Space No One Can Hear You Stream
Martin Baillon, Assia Mahboubi and Pierre-Marie Pédrot.
Contextual Metaprogramming for Session Types
Pedro Ângelo, Atsushi Igarashi, Yuito Murase and Vasco T. Vasconcelos.
Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism
Patrycja Balik, Szymon Jędras and Piotr Polesiuk.
Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism
Hasti Toossi and Ningning Xie.
Auditing Rust Crates Effectively
Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan and Caleb Stanford.
Code Generation via Meta-programming in Dependently Typed Proof Assistants
Mathis Bouverot-Dupuis and Yannick Forster.
|
TACAS: Static Analysis & Program Verification
Room: Sala 500
ReCheck: Automated Contextual Improvement Verifier for Functional Calculi across User-Defined Operational Semantics
Makoto Hamana and Kento Emoto
On Deciding Constant Runtime of Linear Loops
Florian Frohn, Jürgen Giesl, Peter Giesl and Nils Lommen.
Data Structure Analysis for Binaries
Sadra Bayat Tork, Nicholas Coughlin, Alicia Michael, James Tobler and Kirsten Winter
Integrating String Reasoning in Symbolic Execution of C Programs
Rachel Cleaveland and Clark Barrett.
Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Tree
Nat Karmios, Sacha-Elie Ayoun and Philippa Gardner.
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
|
Industry Day
Chair: Nikolai Kosmatov
Room: Sala Madrid
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)
Toward a scalable methodology for Automating Safety Analysis
Stefano Minopoli (Collins Aerospace)
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
|
|
19:00
|
ETAPS Banquet
Room: Giardino Delle Meraviglie
|
|
09:00
|
Guy Van Den Broeck: Symbolic Reasoning in the Age of Large Language Models
Room: Sala 500
Chair: Sebastian Junges
|
|
10:00
|
Coffee Break
Room: Expo Area
|
|
10:30
10:50
11:10
11:30
11:50
12:10
|
TACAS: CPS & Quantum
Room: Sala 500
Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination
Lukas König, Christian Schildwächter, Michaela Klauck and Christian Heinzemann.
VeriLHyS: a Framework for LTL Specification and Verification of Hybrid Systems
Ludovico Battista, Stefano Tonetta and Gianni Zampedri.
TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics
S. Akshay, Prerak Contractor, Paul Gastin, R Govind and B Srivathsan.
Trace Repair Using Temporal Behavior Trees
Sebastian Schirmer, Philipp Schitz, Johann C. Dauer, Bernd Finkbeiner and Sriram Sankaranarayanan.
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.
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
A Category-Theoretic Framework for Dependent Effect Systems
Satoshi Kura, Marco Gaboardi, Taro Sekiyama and Hiroshi Unno.
Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs
Han Xu and Di Wang.
Max-Policy Iteration, Revisited
David Monniaux and Helmut Seidl.
Complete Abstractions for Verification of Polymorphic Functions with Equality
Malo Revel, Thomas Genet and Thomas Jensen.
Modular Automatic Complexity Analysis of Recursive Integer Programs
Nils Lommen and Jürgen Giesl.
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
|
|
12:30
|
Lunch Break
Room: Expo Area
|
|
14:00
14:20
14:40
15:00
15:20
15:40
16:00
|
TACAS: Model Checking & Hardware Verification
Room: Sala 500
CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems
Roberto Pettinau and Christoph Matheja.
Verifying First-Order Temporal Properties of Infinite States Systems via Timers and Rankings
Raz Lotan, Neta Elad, Oded Padon and Sharon Shoham.
Revisiting Stateful Partial-Order Reduction
Frédéric Herbreteau, Gérald Point and Igor Walukiewicz.
Deconstructing Subset Construction: Reducing While Determinizing
Markus Frohme and John Nicol.
ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang and Cunxi Yu
EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
Guangyu Hu, Xiaofeng Zhou, Wei Zhang and Hongce Zhang.
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
|
Test-Comp
Chair:
Room: Sala Madrid
|
SPIN
Chair:
Room: Sala Parigi
|
|
16:00
|
Coffee Break
Room: Expo Area
|
|
16:30
16:50
17:10
17:30
17:50
18:10
|
TACAS: SAT/SMT II
Room: Sala 500
Parallel SMT Solving via Iterative Tree Partitioning
Tomáš Kolárik, Antti E.J. Hyvärinen, Seyedmasoud Asadzadeh and Natasha Sharygina.
Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob
Dominik Schreiber, Aina Niemetz and Mathias Preiner.
Exploring the SMT-LIB Benchmark Library
Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Pascal Fontaine, Cesare Tinelli and Clark Barrett.
SMT(LIA) Sampling with High Diversity
Yong Lai, Junjie Li and Chuan Luo.
BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability
Jakub Horák and Martin Jonáš.
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
|
SPIN
Chair:
Room: Sala Parigi
|