Polyregular Model Checking
Formal Languages and Automata Theory
2025-05-16 v2
Abstract
We introduce a high-level language with Python-like syntax for string-to-string, polyregular, first-order definable transductions. This language features function calls, boolean variables, and nested for-loops. We devise and implement a complete decision procedure for the verification of such programs against a first-order specification. The decision procedure reduces the verification problem to the decidable first-order theory of finite words (extensively studied in automata theory), which we discharge using either complete tools specific to this theory (MONA), or to general-purpose SMT solvers (Z3, CVC5).
Cite
@article{arxiv.2503.18514,
title = {Polyregular Model Checking},
author = {Aliaume Lopez and Rafał Stefański},
journal= {arXiv preprint arXiv:2503.18514},
year = {2025}
}