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 _________________________ Racket Developers list: http://lists.racket-lang.org/dev