Modeling Systems in CLP

12 years 1 months ago
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...
Joxan Jaffar, Andrew E. Santosa, Razvan Voicu
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where ICLP
Authors Joxan Jaffar, Andrew E. Santosa, Razvan Voicu
Comments (0)