The DisCo Home Page

Formal Verification of Disco Specifications

Because of the formal basis of the DisCo specification language, temporal properties of DisCo specifications may be verified formally. Doing large proofs by hand is an error prone process, and therefore we provide support for mechanical reasoning.

The compiler in the current implementation of the animation tool has been modified to produce theories in the logic of the PVS theorem prover. We can currently reason about invariance properties, but liveness properties could be treated as well.

A simple example of verifications undertaken with the tool is:

a simple taxi cab system that illustrates the system,

Give feedback.