Néstor Cataño's proposal on "B2Dafny: Extending Boogie to Support the Analysis of B Machines" has been granted a SEIF-2011 (Software Engineering Innovation Foundation) award by Microsoft Research. Microsoft Research is very active in promoting and encouraging the development of software engineering research, and with the SEIF awards it aims at supporting academic research in software engineering technologies, tools, and education. Microsoft Research awards 12 SEIF projects every year, and this year three researchers have been awarded in Europe, namely, Bashar Nuseibeh at The Open University in UK, Filippo Lanubile at the University of Bari in Italy, and Néstor Cataño at M-ITI. The work proposed by Néstor Cataño will extend the Boogie tool, developed at Microsoft Research, to support the analysis of specifications expressed in the predicate calculus. The work is useful for a number of reasons. It will grant Boogie access to a vast formal methods community using refinement calculus to develop software. And it will allow people working in the refinement calculus to have access to an ample set of formal techniques (e.g. runtime checking and static analysis) and tools, providing quick feedback about the correctness of programs. The difference is that, due to the popularity of C# and the automation power of Boogie, a wider range of problems and audiences could fall within the scope of Boogie.
The SEIF-2011 awards will be launched at the Software Summit in Paris on April 13 to 15, and at the International Conference of Software Engineering on May 21 to 28 in Honolulu, Hawaii.
