Wolfgang Jeltsch wrote:
Hello,
where can I find information about formal verification techniques and tools
for functional programming languages? Both introductionary texts and current
research papers etc. are welcome.
See the specification language HasCASL. For specification of monadic
programs, we have developed a Hoare calculus and a dynamic logic,
which are also represented in the theorem prover Isabelle.
Related is the Heterogeneous Tool Set.
http://www.tzi.de/agbkb/forschung/formal_methods/CoFI/HasCASL/
http://www.tzi.de/cofi/hets
The Isabelle tutorial has some examples from functional programming
http://www4.in.tum.de/~nipkow/LNCS2283/
Also, P-logic and the Programatica tool should be of interest:
ftp://ftp.cse.ogi.edu/pub/pacsoft/papers/Plogic.pdf
http://www.cse.ogi.edu/PacSoft/projects/programatica/
Greetings,
Till
--
Till Mossakowski Phone +49-421-218-4683
Dept. of Computer Science Fax +49-421-218-3054
University of Bremen [EMAIL PROTECTED]
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
