[darcs-devel] Combining Verification Methods for Darcs
Patrik Jansson
patrikj at cs.chalmers.se
Tue Apr 26 08:18:57 PDT 2005
I work at Chalmers in the Cover project (COVERproject.org) and we have
recently started to use the Darcs source code as a case study for our
verification tools. Darcs already contains some QuickCheck properties
and we will try to use first order logic theorem proving as well (with
automatic translation from Haskell using CoverTranslator). So far we
have only got to the point of being able to run the CoverTranslator on
some of the Patch* modules, without actually proving anything
interesting. But we will continue to improve the tool with the aim to
proving (or disproving;-) a few properties of the Patch algebra.
(I just thought you might be interested in knowing that the code you
write is used for more than its primary purpose;-)
So far we have been finding CoverTranslator bugs but if all goes well we
could actually help shaking out a few bugs from Darcs itself.
Kind regards,
Patrik Jansson
More information about the darcs-devel
mailing list