[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