Modal Kleene Algebra Applied to Program Correctness
21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, FM 1016: Formal Methods
MetadataShow full item record
Borges Ferreira Gomes, V., & Struth, G. (2016). Modal Kleene Algebra Applied to Program Correctness. 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, FM 1016: Formal Methods, 9995 https://doi.org/10.1007/978-3-540-27815-3_30
Modal Kleene algebras are relatives of dynamic logics that support program construction and verification by equational reasoning. We describe their application in implementing versatile program correctness components in interactive theorem provers such as Isabelle/HOL. Starting from a weakest precondition based component with a simple relational store model, we show how variants for Hoare logic, strongest postconditions and program refinement can be built in a principled way. Modularity of the approach is demonstrated by variants that capture program termination and recursion, memory models for programs with pointers, and program trace semantics.
Engineering and Physical Sciences Research Council (Grant ID: REMS: Rigorous Engineering for Mainstream Systems, EP/K008528/1)
External DOI: https://doi.org/10.1007/978-3-540-27815-3_30
This record's URL: https://www.repository.cam.ac.uk/handle/1810/260625