[racket-dev] Announcing Soft Contract Verification tool

Racketeers,

Over the last year, we've been working on a tool for automatically
verifying that programs live up to their contracts. We're happy to
announce that it's now available for people to try out here:

   http://scv.umiacs.umd.edu

You type in some modules in the editor, and click either Run or
Verify. The Verify button uses our tool to determine if the modules
always live up to their contract, and if they don't, it automatically
generates a counterexample, showing how to break the module. There are
a number of examples that you can play with, accessed via a menu on
the site.

Right now, the tool supports a fixed subset of Racket, but we're
working on making it handle much more by analyzing fully-expanded
programs.

There's explanations on the site to go along with each example
program, and there's an "About" page with more info, and links to our
papers about the work, at http://scv.umiacs.umd.edu/about

We plan to release a command-line tool and a DrRacket plugin in the
future, once we can handle more of Racket.

If you have questions, comments, bugs, or any other feedback, let us
know, or just file bug reports on the GitHub source code.

Phil, David, Sam