Research

TOPL is a runtime verifier of temporal properties for Java programs.

Utilities

HomeworkEval is a web application I used to quickly grade programming homeworks.

Old Research

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