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 till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till