14:00
15:00
We reduce the model checking problem for a subset of Python to
the satisfiability of a first-order formula over finite words, which is
known to be decidable. The reduction is based on the theory of
polyregular functions, a recently developed generalization of regular
languages to polynomial output string-to-string functions. We
implemented this reduction in a verification tool called PolyCheck, that
can use both automata-based solvers and classical SMT solvers as
backends.
This is a joint work with Rafał Stefański that was pursued
at the University of Warsaw, and was published at CAV'2025.
LaBRI