Polyregular model checking

Prelegent(ci)

Rafał Stefański

Afiliacja

University of Warsaw

Język referatu

angielski

Termin

19 lutego 2025 14:15

Pokój

p. 5440

Tytuł w języku polskim

Polyregular model checking

Seminarium

Seminarium „Teoria automatów”

---

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 Aliaume Lopez.

---