Are you familiar with Hoare and Misra's Verification Grand Challenge? Here are a couple of pointers to recent workshops http://www.csl.sri.com/users/shankar/VGC05/ and http://vstte.ethz.ch/index.html FWIW, I personally feel that transforming specifications into programs via synthesis or refinement or whatever is going to net you a better return than after the fact verification. That's just IMHO. Right now I'm looking at different possibilities for specification languages, and I feel that Haskell gets you 70-80% of the way there (I think that Hoare himself said something along those lines sometime back) cheers "Wolfgang Jeltsch" <wolfgang@jeltsch.net> wrote in message news:200511041213.04185.wolfgang@jeltsch.net...
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.
Best wishes, Wolfgang