Modeling Systems in CLP

We present a methodology for the modeling of complex program behavior in CLP. In the first part we present an informal description about how to represent a system in CLP. At its basic level, this representation captures the 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 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 coinductive tabling to CLP. Essentially, this extends CLP so that it can inductively use p...

• Type: Conference
• Year: 2005
• Where: ICLP
• Authors: Joxan Jaffar, Andrew E. Santosa, Razvan Voicu
• Keywords: CLP Interpreter, Clp Programs, General Clp, ICLP 2005, Programming Languages