POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Wed 14 Jan 2026 11:45 - 12:10 at Réfectoire - Automata 1 Chair(s): Andreas Pavlogiannis

We present the first fully automatic framework for verifying relational properties of \emph{parameterized quantum programs}, i.e., a program that, given an input size, generates a corresponding quantum circuit. We focus on verifying input-output correctness as well as equivalence. At the core of our approach is a new automata model, synchronized weighted tree automata (SWTAs), which compactly and precisely captures the infinite families of quantum states produced by parameterized programs. We introduce a class of transducers to model quantum gate semantics and develop composition algorithms for constructing transducers of parameterized circuits. Verification is reduced to functional inclusion or equivalence checking between SWTAs, for which we provide decision procedures. Our implementation demonstrates both the expressiveness and practical efficiency of the framework by verifying a diverse set of representative parameterized quantum programs with verification times ranging from milliseconds to seconds

Wed 14 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

10:30 - 12:10
Automata 1POPL at Réfectoire
Chair(s): Andreas Pavlogiannis Aarhus University
10:30
25m
Talk
Bounded Treewidth, Multiple Context-Free Grammars, and Downward ClosuresRemote
POPL
C. Aiswarya Chennai Mathematical Institute, Pascal Baumann MPI-SWS, Prakash Saivasan Institute of Mathematical Sciences, Lia Schütze MPI-SWS, Georg Zetzsche MPI-SWS
DOI
10:55
25m
Talk
Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its ApplicationsDistinguished Paper
POPL
Aurèle Barrière EPFL, Victor Deng EPFL; École Normale Supérieure - PSL - CNRS, Clément Pit-Claudel EPFL
DOI Pre-print
11:20
25m
Talk
Network Change Validation with Relational NetKAT
POPL
Han Xu Princeton University, Zachary Kincaid Princeton University, Ratul Mahajan University of Washington, Intentionet, David Walker
DOI
11:45
25m
Talk
Parameterized Verification of Quantum Circuits
POPL
Parosh Aziz Abdulla Uppsala University; Mälardalen University, Yu-Fang Chen Academia Sinica, Michal Hečko Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Ramanathan S. Thinniyam Uppsala University
DOI