- 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 )