PROGRAM REASONING WITH CLP

(web page under construction!)

Formal reasoning of programs for discovering and proving properties of programs is crucially needed and yet their development and large-scale deployment is in its infancy. We are developing a highly flexible framework for general program reasoning that attempts to bridge this gap. We start by modeling programs in the framework of Constraint Logic Programming (CLP), which is highly expressive for behavioral modeling of systems, including those of programs and specifications. In particular, the support for constraints allows for a flexible modeling of complex behavior. By executing the model CLP program, the system's run can be straightforwardly simulated.

To achieve our goal, we are developing a generic implementation based on adapting the best-known CLP techniques, in particular to engineer methods in inductive tabling to record partial reasoning results during run. We are also designing new solvers to reason about complex recursive datatypes commonly occurring in programs.

The implementation incorporates a novel search algorithm which employs interpolation technique to compute maximal abstraction of the problem which preserves the desired property. Taking advantage of CLP as a programming system, the implementation is highly tunable, making it easier for the user to optimize it according to the reasoning problem at hand. The implementation has been applied to program resource usage analysis, static slicing, program verification, and even constraint solving.

Representative Publications

• J. Jaffar, A. E. Santosa. Recursive Abstractions for Parameterized Systems. In A. Cavalcanti and D. Dams Eds. FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2009, Proceedings. pp. 72-88, LNCS 5850, Springer, 2009.
• J. Jaffar, A. E. Santosa, and R. Voicu. An Interpolation Method for CLP Traversal. In I. P. Gent, ed. Principles and Practice of Constraint Programming - CP 2009. 15th International Conference, CP 2009, Lisbon, Portugal, September 2009, Proceedings. pp. 454-469, LNCS 5732, Springer, 2009.
• J. Jaffar, A. E. Santosa, and R. Voicu. A Coinduction Rule for Entailment of Recursively-Defined Properties. In P. J. Stuckey, ed. Constraint Programming: Proceedings of the 14th International Conference on Principles and Practice of Constraint Programming, Sydney, Australia, 14--18 September 2008. pp. 493-508, LNCS 5202, Springer, 2008.
• J. Jaffar, A. E. Santosa, and R. Voicu. Efficient Memoization for Dynamic Programming with Ad-Hoc Constraints. In the Proceedings of AAAI '08. Pages 297-303.