Software Property Specification

Extraction of checkable models is just one piece of the puzzle. Another key impediment to the use of finite-state verification tools in practice is the problem of encoding statements of system correctness requirements in the formal languages that those tools take as input. The Specification Patterns project addresses that problem. The patterns work has recently been integrated with Bandera.