Joose stands for Java-based Object-Oriented Symbolic Executor. This is a simple language and tool for writing asserted Object-Oriented programs and then proving them correct. It started as a project I undertook for Professor Kemmerer at UCSB. It grew into a young open source project before the project was superceded by Omnibus.

Screenshot of the Joose IDE

"Joose: Java-based Object-Oriented Symbolic Executor" (revised version) , (original version)
- (Submitted to Professor Kemmerer as part of project for CS266 at UCSB on 7th June 2002)
- Presents a high-level overview of the Joose language and IDE
"Class verification and object manipulation in Joose" (revised version) , (original version)
- (Submitted to Professor Kemmerer as part of project for CS266 at UCSB on 7th June 2002)
- Presents the details of the techniques used by the Joose verification tool, focussing on extensions needed to support OOP