Polyregular model checking

Speaker(s)

Rafał Stefański

Affiliation

University of Warsaw

Language of the talk

English

Date

Feb. 19, 2025, 2:15 p.m.

Room

room 5440

Title in Polish

Polyregular model checking

Seminar

Seminar Automata Theory

---

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.

---