Mini-course around Event-B and Rodin: hypervisor

Event-B is a method for the stepwise development of programs. The development is mostly top-down and gradually introduces details, rather than starting at the concrete level of writing code. The Event-B method is implemented in the Rodin tool.

This lecture gives a status report of the hypervisor we are developing using Event-B.

Speaker Details

Jean-Raymond Abrial is the co-inventor of Z, B and Event-B. He is the author of the “B-book” (CUP 1996), which presents the B-Method. He published recently a new book “Modeling in Event-B: System and Software Engineering” (CUP 2010). He was a guest Professor at ETH Zurich from 2004 to 2007 where he led the team developing the Rodin Platform for Event-B (funded by the European Project Rodin). After that, he was a researcher also at ETH Zurich, working on a new European Project called Deploy till May 2009. Before being in Zurich, he was a consultant for more than 20 years working in close contact with industrial companies but also with various universities around the world.

Rustan Leino is a Principal Researcher in the RiSE group at Microsoft Research, Redmond.

Date:
Speakers:
Jean-Raymond Abrial and Rustan Leino
Affiliation:
MSR
    • Portrait of Jeff Running

      Jeff Running

    • Portrait of Rustan Leino

      Rustan Leino

      Principal Researcher