Local completeness logic on Kleene algebra with tests

DOI10.1007/978-3-031-22308-2_16MaRDI QIDQ6164436zbMATH OpenFDO

Authors Marco Milanese, Francesco Ranzato

Publication date 28 July 2023

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2205.08128, http://www.math.unipd.it/~ranzato/papers/sas22.pdf

zbMATH Keywords

complete abstract interpretationincorrectness logicKleene algebra with testslocal completeness logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Local Completeness Logic (LCL) has been put forward as a program logic for proving both the correctness and incorrectness of program specifications. LCL is an abstract logic, parameterized by an abstract domain that allows combining over- and under-approximations of program behaviors. It turns out that LCL instantiated to the trivial singleton abstraction boils down to O'Hearn incorrectness logic, which allows us to prove the presence of program bugs. It has been recently proved that suitable extensions of Kleene algebra with tests (KAT) allow representing both O'Hearn incorrectness and Hoare correctness program logics within the same equational framework. In this work, we generalize this result by showing how KATs extended either with a modal diamond operator or with a top element are able to represent the local completeness logic LCL. This is achieved by studying how these extended KATs can be endowed with an abstract domain so as to define the validity of correctness/incorrectness LCL triples and to show that the LCL proof system is logically sound and, under some hypotheses, complete.

Recommendations

• On Hoare logic and Kleene algebra with tests
• Deciding KAT and Hoare logic with derivatives
• Logics for extensional, locally complete analysis via domain refinements
• scientific article; zbMATH DE number 2090029

Cites work

• A coalgebraic decision procedure for NetKAT
• A fast compiler for NetKAT
• Algebras of modal operators and partial correctness
• An axiomatic basis for computer programming
• Analyzing program analyses
• Cantor meets Scott: semantic foundations for probabilistic networks
• Complete abstractions everywhere
• Equational theories of abnormal termination based on Kleene algebra
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• Incorrectness logic for graph programs
• Kleene algebra with domain
• Local reasoning about the presence of bugs: incorrectness separation logic
• Making abstract interpretations complete
• Netkat, semantic foundations for networks
• On algebra of program correctness and incorrectness
• On Hoare logic and Kleene algebra with tests
• Propositional dynamic logic of regular programs
• Systematic design of program transformation frameworks by abstract interpretation

Cited in

(6)

• Locality and Applications to Subsumption Testing in EL and Some of its Extensions
• On Hoare logic and Kleene algebra with tests
• Logic for reasoning about bugs in loops over data sequences (IFIL)
• Embedding Kozen-Tiuryn logic into residuated one-sorted Kleene algebra with tests
• A correctness and incorrectness program logic
• Local variable scoping and Kleene algebra with tests

This page was built for publication: Local completeness logic on Kleene algebra with tests

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6164436)