Student Work

Random finite-state automata for model checking

Public

Formal verification has been very successful in hardware design, and its extension to software is hindered by the large finite-state automata models of modern programs. To provide a basis upon which to evaluate and improve verification algorithms, our software generates random finite-state automata with imposed structural constraints. These constraints are controlled by four different algorithms which can additionally be composed. In order to enable verification algorithm evaluations, the software exports generated finite-state automata as modules in the Verilog language which can be loaded into a model checker called VIS.

  • This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.
Creator
Publisher
Identifier
  • 02C027M
Advisor
Year
  • 2002
Date created
  • 2002-01-01
Resource type
Major
Rights statement

Relations

In Collection:

Items

Items

Permanent link to this page: https://digital.wpi.edu/show/k35697624