Over a period of some 6-7 years the FDT group at SICS and KTH has explored the use of first-order mu-calculus as a framework for program verification. In the talk I will cover the theorem-proving foundations of this work, in particular the lazy handling of induction and coinduction, ways of embedding programming languages and logics into the framework, and applications to the Erlang programming language.
| Mads Dam |
| Associate Professor at SICS and
IMIT/KTH, Stockholm Visitor to the NICTA Formal Methods Program |
| Date: | Tue Nov 23 2004 |
| Time: | 1pm to 2pm |
| Location: | Level 10 meeting room, Applied Science Bldg (F10), UNSW Kensington campus |
| Materials: | pdf, ppt |
Last updated by tbourke at Tue Nov 23 15:24:10 2004 GMT+1100