[Developer] uml

[Gernot Heiser]

>>>>> On Fri, 4 May 2007 00:29:20 -0400, "Jorge Torres" <jorge.torres.maldonado at gmail.com> said:
JT> [...]

JT> I have one question, why did you decided not to continue the verification with
JT> event-b?

We never had a verification project using B. We had a student project
on formalising the V4 API that used B (mostly because that was what
the student was familiar with, and it has nice visualisation). This
was in parallel with the verification pilot project, which already
used Isabelle.

Using B for the verification was never really considered, people were
convinced from the beginning that Isabelle/HOL was the right
environment.

Gernot