{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,29]],"date-time":"2023-05-29T09:10:49Z","timestamp":1685351449152},"reference-count":4,"publisher":"National Library of Serbia","issue":"2","license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ComSIS","COMPUT SCI INF SYST","COMPUT SCI INFORM SY","COMPUTER SCI INFORM","COMSIS J"],"published-print":{"date-parts":[[2008]]},"abstract":"<jats:p>In this article we describe an implementation of Kleene algebra with tests (KAT) in the Coq theorem prover. KAT is an equational system that has been successfully applied in program verification and, in particular, it subsumes the propositional Hoare logic (PHL). We also present an PHL encoding in KAT, by deriving its deduction rules as theorems of KAT. Some examples of simple program's formal correctness are given. This work is part of a study of the feasibility of using KAT in the automatic production of certificates in the context of (source-level) Proof-Carrying-Code (PCC). .<\/jats:p>","DOI":"10.2298\/csis0802137p","type":"journal-article","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T07:29:02Z","timestamp":1238138942000},"page":"137-160","source":"Crossref","is-referenced-by-count":3,"title":["KAT and PHL in Coq"],"prefix":"10.2298","volume":"5","author":[{"given":"David","family":"Pereira","sequence":"first","affiliation":[{"name":"University of Porto, DCC-FC & LIACC, Porto, Portugal"}]},{"given":"Nelma","family":"Moreira","sequence":"additional","affiliation":[{"name":"University of Porto, DCC-FC & LIACC, Porto, Portugal"}]}],"member":"1078","reference":[{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2960"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343378"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116"}],"container-title":["Computer Science and Information Systems"],"original-title":[],"language":"en","deposited":{"date-parts":[[2023,5,29]],"date-time":"2023-05-29T08:29:35Z","timestamp":1685348975000},"score":1,"resource":{"primary":{"URL":"https:\/\/doiserbia.nb.rs\/Article.aspx?ID=1820-02140802137P"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"references-count":4,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008]]}},"URL":"https:\/\/doi.org\/10.2298\/csis0802137p","relation":{},"ISSN":["1820-0214","2406-1018"],"issn-type":[{"value":"1820-0214","type":"print"},{"value":"2406-1018","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}