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: | , , |
|---|---|
| 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 |
| _version_ | 1811289008050798592 |
|---|---|
| author | Ricardo Almeida Sabine Broda Nelma Moreira |
| author_facet | Ricardo Almeida Sabine Broda Nelma Moreira |
| author_sort | Ricardo Almeida |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-13T03:47:22Z |
| format | Article |
| id | doaj.art-dc3767446a714ae897f5ebea471f01df |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T03:47:22Z |
| publishDate | 2012-10-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-dc3767446a714ae897f5ebea471f01df2022-12-22T03:03:58ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-10-0196Proc. GandALF 201212714010.4204/EPTCS.96.10Deciding KAT and Hoare Logic with DerivativesRicardo AlmeidaSabine BrodaNelma MoreiraKleene 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.http://arxiv.org/pdf/1210.2456v1 |
| spellingShingle | Ricardo Almeida Sabine Broda Nelma Moreira Deciding KAT and Hoare Logic with Derivatives Electronic Proceedings in Theoretical Computer Science |
| title | Deciding KAT and Hoare Logic with Derivatives |
| title_full | Deciding KAT and Hoare Logic with Derivatives |
| title_fullStr | Deciding KAT and Hoare Logic with Derivatives |
| title_full_unstemmed | Deciding KAT and Hoare Logic with Derivatives |
| title_short | Deciding KAT and Hoare Logic with Derivatives |
| title_sort | deciding kat and hoare logic with derivatives |
| url | http://arxiv.org/pdf/1210.2456v1 |
| work_keys_str_mv | AT ricardoalmeida decidingkatandhoarelogicwithderivatives AT sabinebroda decidingkatandhoarelogicwithderivatives AT nelmamoreira decidingkatandhoarelogicwithderivatives |