[plt-scheme] Regarding research on formal methods and verification of software in Scheme

[Matthias Felleisen]

On Dec 14, 2006, at 9:53 AM, Paulo J. Matos wrote:

> Hello all,
>
> I would like some insight and references from the people in the Scheme
> Research world on work done regarding software verification in Scheme
> with Formal or Semi formal methods. For example, for
> property/assertion verification, verification of program correctness a
> posteriori and generation of scheme code from formal specifications,
> be it in B, Z or Alloy.

You may wish to read up on Robby Findler's contract work
  (http://people.cs.uchicago.edu/~robby/pubs/)
or Dale Vaillancourt's Dracula plug-in for DrScheme
  (http://www.ccs.neu.edu/home/dalev/acl2-drscheme/index.html)

-- Matthias