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

...

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?

Graham Hutton's _Programming in Haskell_ has a chapter on reasoning about Haskell code: http://www.cs.nott.ac.uk/~gmh/book.html I put together some exercises of some short proofs for small Haskell functions: http://www.thenewsh.com/~newsham/formal/problems/ I have a short article that covers proofs in Haskell and Isabelle: http://users.lava.net/~newsham/formal/reverse/ The seL4 project is specifying an OS in Haskell, proving it in Isabelle and translating it to C with proofs that connect the translations: http://ertos.nicta.com.au/research/sel4/ I have an article on the curry-howard correspondence http://www.thenewsh.com/~newsham/formal/curryhoward/ In systems like Coq you can write code and proofs of the code in the same language and even at the same time. The Coq'Art book is a good reference, as are Adam Chlipala's draft book and Harvard class materials and the _Type Theory & Functional Programming_ book. Full text for all but Coq'Art are online: http://www.labri.fr/perso/casteran/CoqArt/index.html http://www.cs.harvard.edu/~adamc/cpdt/ http://www.cs.harvard.edu/~adamc/cpdt/book/ http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/

Denis

Tim Newsham http://www.thenewsh.com/~newsham/

On Mon, Feb 2, 2009 at 10:04 PM, 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.

Any references to publications related to this?

-- Don

-- Paulo Jorge Matos - pocmatos at gmail.com Webpage: http://www.personal.soton.ac.uk/pocm

Excerpts from Austin Seipp's message of Tue Feb 03 03:40:47 -0600 2009:

...

After noticing that I didn't give a link to the code in the last message, I searched and found this more up to date page I think: http://compcert.inria.fr/doc/index.html

Austin