- Develop a standalone application that implements an LTL model checker
- Use the Java path finder and kodkod SAT library to verify functional correctness of a given concurrent implementation of the red black tree
- Use the Java path finder to verify various properties of an example concurrent system (e.g. a single lane bridge control system or a cruise control system )