Projekte
- LWAASpin, eine Modifizierung des SPIN-Model Checker um Tarjans Algorithmus und die Verwendung linearer schwacher alternierender Automaten
- Visualisierung von Zustandsräumen expliziter Model Checker
- CMC, ein komponentenbasierter, disk-based Model Checker
- (Eine Liste verschiedener Model Checker)
- Ein extrem effizienter Handevaluator für "best 5 out of 7 cards"-Poker-Spiele (e.g., Texas Hold'em)
- Eine "virtuelle" virtuelle Maschine für Java: Ausführen von Java-Programmen in Java, mit direkter Kontrolle über die Ausführung des Bytecodes.