TOPL is a runtime verifier of temporal properties for Java programs.
HomeworkEval is a web application I used to quickly grade programming homeworks.
jStar is a Java program verifier that uses separation logic for annotations. The main authors are Matthew Parkinson and Dino Distefano; I used to help improve it. (You should use Facebook's Infer, though.)
FreeBoogie is a verification condition generator for the Boogie language. I used it during my PhD work to do some experiments, because Boogie was not open source at the time.
ESC/Java is a static verifier for Java programs annotated with JML. I implemented a big part of the reachability analysis that is activated by the -era flag.
CLOPS is a domain specific language, a tool, and a library that make it easy to write Java programs with a command line interface. I contributed to its design.
Fx7 is an SMT solver. I wrote a small module for simplifying formulas in certain circumstances.
Last updated: 18 December 2016