SRTool is a verification tool for programs in Simple C, a variant of C that was part of the 440 Software Reliability course at Imperial College London. The course involves a significant piece of coursework (worth 33% of the mark for the module), requiring students to implement a tool that checks these programs to determine if they satisfy their specifications or not. Of course, the problem is undecidable in general; the tool is allowed to report UNKNOWN for programs it isn’t sure about, as giving wrong answers is negatively marked. Students are given considerable freedom of implementation decisions, algorithms and strategies.
Tom Burnell and I had the 3rd best performance overall in our cohort, scoring 95.5% for accuracy (and 97% overall). We did this by running several analyses in parallel; in addition to the standard static program verification techniques taught as part of the course, we also refined said techniques, implemented variants of bounded model checking, automated invariant inference as well as compilation of Simple C programs down into C.
I’ve kept the repository private (to avoid students doing this task in future years from easily copying off too much of the code), but am happy to share details and/or parts of the code should readers be interested.