First Steps Toward Realising the Verified Software Grand Challenge: Coordinating American and European Java Verification Research and Development

Funded by the Enterprise Ireland International Coordination/Travel Program (2005)

Original Abstract

Many researchers in software verification focus on Java programs annotated with the Java Modeling Language (JML). A new major tool effort has recently begun, led by Dr. Kiniry, under the auspices of an E.U. FP6 grant entitled MOBIUS which aims at providing a prototype realisation of Tony Hoare's Verifying Compiler Grand Challenge. The intent of this travel program is to coordinate North American and European development on this tool and its associated underlying theory.