English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Kleene algebra with tests (KAT) is a foundational equational framework forreasoning about programs, which has found applications in programtransformations, networking and compiler optimizations, among many other areas.In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic,showing that one can reason about the (partial) correctness of while programsby means of the equational theory of KAT. In this work, we investigate thesupport that KAT provides for reasoning about incorrectness, instead, asembodied by Ohearn's recently proposed incorrectness logic. We show that KATcannot directly express incorrectness logic. The main reason for thislimitation can be traced to the fact that KAT cannot express explicitly thenotion of codomain, which is essential to express incorrectness triples. Toaddress this issue, we study Kleene Algebra with Top and Tests (TopKAT), anextension of KAT with a top element. We show that TopKAT is powerful enough toexpress a codomain operation, to express incorrectness triples, and to proveall the rules of incorrectness logic sound. This shows that one can reasonabout the incorrectness of while-like programs by means of the equationaltheory of TopKAT.

On Incorrectness Logic and Kleene Algebra with Top and Tests