PROJECT: Constraint-based Search in Program Analysis

Description

Recent advances in program analysis and verification increasingly involve general search techniques, for example, binary decision diagrams in explicit-state-based model checking, SAT-based model checking for programs represented as logical formulas, and more recently, the use of multisorted decision procedures in "SAT Modulo Theory" (SMT) verifiers to reason about complex data types.

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 )

PROJECT: Logical Data Structures

Description

Automated reasoning about programs, as performed by advanced compilers and program analyzers, remain challenged by the use of dynamically allocated data structures. This is essentially because reasoning about a memory model and memory operations is inherently difficult, and hence expressive and efficient algorithms have yet to emerge. This problem is particularly important because many programs use such data structures.

Recently there have been new approaches utilizing Constraint Logic Programming. In particular, constraints capture the underlying memory model while recursive rules capture the user-defined properties. The project is to develop this CLP metholodogy further and engineer new algorithms for practical use in program analyzers.

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 http://www.comp.nus.edu.sg/~joxan/res.html)