Re: [Haskell-cafe] Verifying Haskell Programs

dbueno:

On Mon, Feb 2, 2009 at 15:04, Don Stewart wrote:

...

pocmatos:

...

Hi all,

Much is talked that Haskell, since it is purely functional is easier > to be verified. > However, most of the research I have seen in software verification > (either through model checking or theorem proving) targets C/C++ or > subsets of these. What's the state of the art of automatically > verifying properties of programs written in Haskell?

State of the art is translating subsets of Haskell to Isabelle, and verifying them. Using model checkers to verify subsets, or extracting Haskell from Agda or Coq.

Don, can you give some pointers to literature on this, if any? That is, any documentation of a verification effort of Haskell code with Isabelle, model checkers, or Coq?

(It's not that I don't believe you -- I'd be really interested to read it!)

All on haskell.org, http://haskell.org/haskellwiki/Research_papers/Testing_and_correctness#Verif... And there's been work since I put that list together. -- Don