1. Introduction and software testing
white box testing, black box testing, triangle example, unit testing, JUnit
2. Assertion and property-based testing
assertion, property-based testing, QuickCheck, ScalaCheck
3. Model-based testing
model-based testing, Modbat
4. Software model checking
software model checking, Java PathFinder (JPF)
5. Basic model checking
model checking, SPIN, temporal logic, linear temporal logic (LTL)
6. Software model checking by linear temporal logic
JPF+LTL