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 |
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 |
In reply to this post by Paulo J. Matos
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 |
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 |
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 |
In reply to this post by Don Stewart-2
> 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 |
In reply to this post by Don Stewart-2
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 |
In reply to this post by Don Stewart-2
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 |
In reply to this post by Paulo J. Matos
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 |
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 |
In reply to this post by Denis Bueno
>> 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 |
Free forum by Nabble | Edit this page |