Research

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

jStar is a Java program verifier that uses separation logic for annotations. The main authors are Matthew Parkinson and Dino Distefano; I help improve it.

FreeBoogie is a verification condition generator for the Boogie language.

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 and I might maintain it a bit in the future.

Utilities

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


Last updated: 25 February 2013