VERDECT can be used for the verification of speed-independent or delay-insensitive circuits, in particular control circuits. VERDECT has a simple user interface, can verify safety and various progress conditions, and allows a modular verification.

VERDECT, version 2.3, comes with the following files. Currently we only have an executable for a sparc machine. If you need an executable for another machine or the source code (in C), please let us know.

It's available by ftp from here (

Contact: Jo Ebergen, Computer Science Department, University of Waterloo, Waterloo, Ontario, N2L 3G1 (