Verifying Haskell Programs

[Paulo J. Matos]

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?

Cheers,

--
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Thomas DuBuisson]

On Sun, Feb 1, 2009 at 12:54 PM, Paulo J. Matos <[hidden email]> wrote:
> What's the state of the art of automatically
> verifying properties of programs written in Haskell?

This is a large field that isn't as black and white as many people
frame it.  You can write a proof [1] then translate that into Haskell,
you can write Haskell then prove key functions, using a case totality
checker you could prove it doesn't have any partial functions that
will cause an abnormal exit [2], some research has been performed into
information flow at UPenn [3], and SPJ/Zu have been looking at static
contract checking [4] for some time now - which I hope sees the light
of day in GHC 6.12.  While this work has been going on, folks at
Portland State and a few others (such as Andy Gill [8], NICTA [5], and
Peng Li to an extent) have been applying FP to the systems world [6]
[7].

Hope this helps,
Thomas

[1] Perhaps using Isabelle, isabelle.in.tum.de.
[2] Neil built CATCH for just this purpose (though it isn't in GHC
yet), www-users.cs.york.ac.uk/~ndm/catch/
[3] www.cis.upenn.edu/~stevez/
[4] www.cl.cam.ac.uk/~nx200/
[5] http://ertos.nicta.com.au/research/l4/
[6] Strongly typed memory areas, http://web.cecs.pdx.edu/~mpj/pubs/bytedata.html
[7] Some work on non-inference as well as thoughts on building a
hypervisor, http://web.cecs.pdx.edu/~rebekah/
[8] Timber language - no, I haven't looked at it yet myself.
http://timber-lang.org/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Don Stewart-2]

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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Denis Bueno]

On Mon, Feb 2, 2009 at 15:04, Don Stewart <[hidden email]> 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!)

                              Denis
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Don Stewart-2]

dbueno:

> On Mon, Feb 2, 2009 at 15:04, Don Stewart <[hidden email]> 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#Verifying_Haskell_programs

And there's been work since I put that list together.

-- Don
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Stefan Monnier]

> 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.

Another state of the art is to use type classes, GADTs, and/or type
functions, to specify and prove the properties you want about
your program.  Basically using similar techniques as used in dependently
typed languages.


        Stefan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Paulo J. Matos]

On Mon, Feb 2, 2009 at 10:04 PM, Don Stewart <[hidden email]> 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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Paulo J. Matos]

On Tue, Feb 3, 2009 at 12:28 AM, Don Stewart <[hidden email]> wrote:

> dbueno:
>> On Mon, Feb 2, 2009 at 15:04, Don Stewart <[hidden email]> 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#Verifying_Haskell_programs
>
> And there's been work since I put that list together.
>

Opps, sorry, missed this message. Should read everything before replying! :)

> -- Don
>



--
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Austin Seipp]

Excerpts from Paulo J. Matos's message of Tue Feb 03 02:31:00 -0600 2009:
> Any references to publications related to this?

While it's not Haskell, this code may be of interest to you:

http://pauillac.inria.fr/~xleroy/bibrefs/Leroy-compcert-06.html

This paper is about the development of a compiler backend using the
Coq proof assistant, which takes Cminor (a C-like language) and
outputs PowerPC assembly code. Coq is used both to program the
compiler and prove it is correct.

Austin
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Austin Seipp]

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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Tim Newsham]

>> 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/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe