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.
Subscribe to:
Post Comments (Atom)
 
 
No comments:
Post a Comment