Output details
11 - Computer Science and Informatics
University of Southampton
Analyzing recursive programs using a fixed-point calculus
Significance of output:
<11>This paper proposes the first declarative framework, Getafix, that easies the development of model-checkers for sequential/concurrent programs based on fixedpoint calculus. Algorithms are defined through a high-level formalism that also allows specification of algorithmic aspects. Within this framework, we develop several model checkers for sequential and concurrent Boolean programs, using a BDD fixed-point engine as backend. This enables building model-checkers that are competitive with state-of-the-art tools. Getafix is the precursor of modern model checkers for general programs built on top of fixed-point engines such as QARMC (TU Munich-Germany), Eldarica (EPFL-Swiss), and Z3-fixedpoints (Microsoft research).