Modeling Systems in CLP with Coinductive Tabling

Joxan Jaffar, Andrew Santosa and Razvan Voicu


We present a methodology for the modelling of complex program behavior in CLP. The first part of this paper is an informal description about how to represent a system in CLP. At its basic level, this representation captures the precise trace semantics of concurrent programs, or even high-level specifications, in the form of a predicate transformer. Based on traces, the method can also capture properties of the underlying runtime system such as the scheduler and the microarchitecture, so as to provide a foundation for reasoning about resources such as time and space.

The second part of this paper presents a formal and compositional proof method for reasoning about safety properties of the underlying system. The idea is that a safety property is simply a CLP goal, and is proof established by executing the goal by a CLP interpreter. However, a traditional CLP interpreter does not suffice. We thus introduce a technique of {\it coinductive tabling} to CLP. Essentially, this extends CLP so that it can inductively use proof obligations that are assumed but not yet proven, and it can generate new proof obligations assertions dynamically.