## 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)