[Haskell] formal verification for functional programming languages
till at informatik.uni-bremen.de
Thu Nov 10 15:17:20 EST 2005
Wolfgang Jeltsch wrote:
> 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.
The Isabelle tutorial has some examples from functional programming
Also, P-logic and the Programatica tool should be of interest:
Till Mossakowski Phone +49-421-218-4683
Dept. of Computer Science Fax +49-421-218-3054
University of Bremen till at tzi.de
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till
More information about the Haskell