Our research area is centered around Constraint Logic Programming (CLP) which has both the components of search and constraint solving. The search process finds refutations to given queries, while constraint solving is used to incrementally simplify theories during search. Therefore, CLP is a paradigm strategically positioned to handle the issues in the latest development of verification.
This project is to develop new search techniques for CLP search. Initial work will involve the evaluation of standard techniques from constraint search such as nogood and clause learning and their use in the context of program analysis. Novelty is then obtainable by exploiting information obtained from the program being verified, as well as techniques from program analysis, such as abstract interpretation.
The student has to have obtained good marks in logic and discrete mathematics-related courses. Familiarity with standard imperative programming languages is assumed, and prior knowledge of constraint solving, program analysis, and a declarative programming language is an advantage.
KEYWORDS: program verification, program analysis, constraint logic programming,logic
(Readings available from here )