Tableaux for verification of datacentric processes

Abstract. Current approaches to analyzing dynamic systems are mostly grounded in propositional (temporal) logics. As a consequence, they often lack expressiv-ity for modelling rich data structures and reasoning about them in the course of a computation. To address this problem, we propose a rich modelling framework based on first-order logic over background theories (arithmetics, lists, records, etc) and state transition systems over corresponding interpretations. On the rea-soning side, we introduce a tableau calculus for bounded model checking of prop-erties expressed in a certain fragment of CTL * over that first-order logic. We also describe a k-induction scheme on top of that calculus for proving safety proper-ties, and we report on first experiments with a prototypical implementation.