2 Feb
2009
2 Feb
'09
5:04 p.m.
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