(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.