Algebraic principles for program correctness tools in Isabelle/HOL
This thesis puts forward a flexible and principled approach to the development of construction and verification tools for imperative programs, in which the control flow and the data level are cleanly separated. The approach is inspired by algebraic principles and benefits from an algebraic semantics...
| Main Author: | |
|---|---|
| Other Authors: | |
| Published: |
University of Sheffield
2015
|
| Subjects: | |
| Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.682305 |