Byron Cook: Student projects

I'm happy to supervise Cambridge students doing Tripos and Diploma projects in the area of automatic program verification. Here are some suggestions:

1. Implement the Octagon abstract domain and simple Octagon-based program analysis in F#. Some pointers:
   • Comprehensive paper on the Octagon domain
   • More information (including online prototype)
   A part of the challenge here is to make a reasonably fast version while staying 100% in F#. Antoine Mine has already developed a fast C-based version.

2. Using F#, implement Rybalchenko and Sofronie-Stokkermans' method for computing linear interpolants. Furthermore, develop a simple program verification tool based on this method using McMillan's methods.

3. Using F#, implement the method of proving non-termination from Gupta et al.'s paper. Develop an interface matching that of RankFinder, then use the tool to prove the validity of counterexamples found by Terminator.