Documentation

• A Brief Description

Details: This document is the same as the one presented at the beginning.

• The reader is referred to the documents below for additional information.

• Syntax Description (VERDS modeling language)

Details: This document explains the syntax of the input model for the verification tool verds.

• The input model is called: verds model, or verds verification model (VVM for short)

• Command Line Options

Details: This document explains the command line options of running the verification tool verds.

• The command line format is of the form: verds [command line options] [input-file]

• Tutorial 1

Details: This document contains a tutorial on specification in VVM and on running verds.

• The tutorial contains two examples: mutual exclusion and leader election

• Tutorial 2 (Part I) and Tutorial 2 (Part II)

Details: The documents contain a tutorial on verification of simple C programs using verds.

• Part I shows the basic verification approach;
• Part II shows the use of assumption-guarantee reasoning.

Some Evaluation Reports

• VERDS version 1.32
• VERDS version 1.30
• VERDS-QBF versus NuSMV