Deciding KAT and Hoare Logic with Derivatives

Ricardo Almeida, Sabine Broda, Nelma Moreira

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 specification and verification of programs, and that is currently the base of most tools for checking program correctness. Both the equational theory of KAT and the encoding of PHL in KAT are known to be decidable. In this paper we present a new decision procedure for the equivalence of two KAT expressions based on the notion of partial derivatives. We also introduce the notion of derivative modulo particular sets of equations. With this we extend the previous procedure for deciding PHL. Some experimental results are also presented.
Original languageEnglish
Title of host publicationProceedings Third International Symposium on Games, Automata, Logics and Formal Verification
EditorsMarco Faella, Aniello Murano
PublisherOpen Publishing Association
Pages127-140
Number of pages14
Volume96
DOIs
Publication statusPublished - 7 Oct 2012
EventThird International Symposium on Games, Automata, Logics and Formal Verification - Napoli, Italy
Duration: 6 Sept 20128 Sept 2012
Conference number: 3

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
ISSN (Electronic)2075-2180

Conference

ConferenceThird International Symposium on Games, Automata, Logics and Formal Verification
Abbreviated titleGandALF 2012
Country/TerritoryItaly
CityNapoli
Period6/09/128/09/12

Fingerprint

Dive into the research topics of 'Deciding KAT and Hoare Logic with Derivatives'. Together they form a unique fingerprint.

Cite this