If you're interested in either of these projects, and have the relevant background, drop me an email at razvan at comp dot nus dot edu dot sg

Safety proofs for self-modifying code

In this project, we define an abstract virtual machine capable of modeling self-modifying code (SMC). That is, the program area of the machine can also be seen as an array of data that can be written into, thus dynamically changing the program being executed. While SMC has multiple applications, we shall consider here only those uses that are specific to embedded systems and lead to improved speed/reduced size of the program. With this view in mind, we define a set of safety properties that would be desirable for a self-modifying program. For instance, one such property would be that write operations occur only to change increment instructions into decrement instructions, and vice versa (this allows efficient conversion of loops from upward-counting to downward-counting, and back).

The purpose of the project is to automate the safety certification process for SMC wrt the safety policy of interest. To this end, we implement a formalization of the SMC semantics in the proof
assistant Coq, and devise automated tactics that discharge safety conditions produced by a verification condition generator.

Tool for loop invariant discovery in simple array programs

Automatic loop invariant generation is an old problem that has been studied since the 70s. While the problem is in general undecidable, there exist currently a variety of heuristics that can generate invariants for certain classes of loops. However, there is no tool that would integrate all these
heuristics together. We would like to address the challenge of building such a tool in this project.

The invariant discovery problem can be abstracted in terms of the transformation that the loop body performs on the data. Moreover, this transformation can be encoded as a constraint-based relationship. For instance, given the simple loop

i = 0; s = 0 ;
while ( i < n ) {
    s = s + i ;
    i = i + 1 ;
}

the loop transformation performed by the loop body can be encoded by the following constraints:

s_new = s_old + i_old && i_new = i_old + 1 && n_old = n_new && i_old < n_old

The tool that we aim to build should process the above constraints into

s = i*(i-1)/2 && i <= n

which is the invariant that holds at the bottom of the loop's body.

An important aspect of this project is to devise a constraint language for arrays and array segments, and to implement heuristics that are able to handle such constraints.