Regular Model Checking Upside-Down: An Invariant-Based Approach

Javier Esparza, Michael Raskin, Christoph Welzel-Mohr

Regular model checking is a technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. The form we a…