[Haskell] Specification and prover for Haskell
gerwin.klein at nicta.com.au
Mon Oct 25 18:32:23 EDT 2010
On 25/10/2010, at 7:09 PM, Romain Demeyer wrote:
> I'm working on static verification in Haskell, and I search for existing works on specification of Haskell programs (such as pre/post conditions, for example) or any other functional language.
We have used Haskell extensively in the verification of the seL4 microkernel. One part of that was translating a prototype of the kernel into Isabelle and proving a large number of invariants as well as proving two refinement theorems about the translation. For our work the translation itself was not correctness critical, so we were happy to use our own somewhat ad-hoc tool for it.
Some papers on this are:
Pre/post verification and refinement of state monad programs:
Experience report on the Haskell verification:
The whole picture:
More papers here:
In general, if your program does not use state monads, but is just a simple, straightforward functional program, the combination of Haskabelle and Isabelle/HOL can work quite nicely without a big formal apparatus such as a pre/post calculus. You can just state properties directly as you might in quickcheck.
> It would be great if there exists a prover based on this kind of specifications. I already found the ESC/Haskell. Do you know some other works which could be interesting?
We're using Isabelle/HOL. In the work above this was together with our own translator from Haskell to Isabelle, in the future it will possibly Haskabelle which has already been pointed out.
More information about the Haskell