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
-
-
Jeff Running
-
Rustan Leino
Principal Researcher
-