Project Title: A Compiler for Symbolic Tracing
  
Job Title: Research Assistant
  
Job Description
  
We are developing a constraint-based verification system targeted at
software written in C and assembly language, capable of verifying
safety and liveness properties. The system will employ (automatic)
search when dealing with finitary properties, and induction for both
finitary and infinitary properties, and user assertions.
  
The research assistant will be involved in the writing of the software,
which largely follows the following guidelines:
  
* Implementations of parsers for C, MIPS assembly language.  These
  parsers will have the option of accepting annotations for the code
  that will be interpreted as assertions.
* Implementation of modeling compiler from C/MIPS into CLP traces.
  The compiler will have the following options:
  - Top-down and bottom-up modeling
  - Modeling input-output relations of program fragments
  - Modeling memory management of C programs
  - Modeling timing of MIPS instructions
* Implementation of CLP-based proof method, with unfolding engine,
  tabling, and interfacing to constraint solvers, model checkers, SAT
  solvers, SMT solvers, and general purpose theorem provers.
* Implementation of array and multiset constraint solvers, which are
  central to our program verification approach.
* A graphical user interface that integrates the entire set of tools
  into an easy-to-use environment.

Requirements

The candidate should posses excellent programming skills in either C,
C++, or Java, preferably with some experience in building graphical
UI.  Knowledge of, and strong interest in, prohram analysis and algorithms,
constraint logic programming, formal logic, and discrete mathematics
would be an advantage.

Remuneration & Benefits

Salary no less than S$ 3,000/mo.

Term of Appointment

The appointment can commence immediately and will be for one year,
with possibility for extension up to one additional year.

Contact Person:

Please send your complete CV to Professor Joxan Jaffar
(joxan@comp.nus.edu.sg)