WCS: a Witness and Counterexample Server

Witness and Counterexample Server (WCS) is planned to be a suite of tools designed to asses the ability of model hecking techniques to increase effectiveness of hardware/software testing activities. It is focused on witnesses and counterexamples produced by model checkers. Currently, a BDD-based model checker with the ability of generating linear witnesses and counterexamples, and witness and counterexample automata is available. Witness and counterexample automata are finite automata recognizing a set of all finite linear witnesses and counterexamples for a given formula over a given model, respectively. WCS is organized as a web service, in order to provide public access to the functionality of verification tools.