|
|
|
|
|
|
by nano_o
4640 days ago
|
|
|
From what I see on the front page, the course seems to be based on the notion of refinement, i.e. transforming a high-level specification into a concrete implementation by refining the specification in several steps.
There is a recent example [1] of a software development process based on refinement. The authors build a fully verified model-checker using Isabelle/HOL. The code has a non-trivial size (4900 lines of ML) and implements complex functionality (model-checking algorithms) in an efficient way. Roughly speaking, it is proved that the model-checker reports the violation of a property if and only if the system under scrutiny does violate the property. [1] http://cava.in.tum.de/templates/publications/CAV2013.pdf |
|
|