Deciding KAT and Hoare Logic with Derivatives
Kleene algebra with tests (KAT) is an equational system for program verification, which is the combination of Boolean algebra (BA) and Kleene algebra (KA), the algebra of regular expressions. In particular, KAT subsumes the propositional fragment of Hoare logic (PHL) which is a formal system for the...
Main Authors: | Ricardo Almeida, Sabine Broda, Nelma Moreira |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2012-10-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1210.2456v1 |
Similar Items
-
Automatic Function Annotations for Hoare Logic
by: Daniel Matichuk
Published: (2012-11-01) -
A Hoare logic for linear systems
by: Arthan, R, et al.
Published: (2013) -
Floyd-Hoare Logic Defines Semantics
by: Meyer, Albert R.
Published: (2023) -
Hoare's Logic Is Not Complete When It Could Be
by: Bergstra, J., et al.
Published: (2023) -
Semantical Considerations on Floyd-Hoare Logic
by: Pratt, Vaughan R.
Published: (2023)