Sunday, January 7, 2018

Verification Corner, Modeling, refinement, and verification


In this episode of Verification Corner, Jean-Raymond Abrial and Rustan Leino show how to do a design starting from a model that is gradually refined toward executable code. They use the Rodin tool, which supports the Event-B formalism.

No comments: