Polyregular Model Checking

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).