Local completeness logic on Kleene algebra with tests

DOI10.1007/978-3-031-22308-2_16zbMath1524.68098arXiv2205.08128MaRDI QIDQ6164436

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

zbMATH Keywords

Kleene algebra with testsincorrectness logiccomplete abstract interpretationlocal completeness logic

Mathematics Subject Classification ID

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

Related Items (1)

Logic for reasoning about bugs in loops over data sequences (IFIL)

Cites Work

• Unnamed Item
• Algebras of modal operators and partial correctness
• Propositional dynamic logic of regular programs
• Incorrectness logic for graph programs
• Local reasoning about the presence of bugs: incorrectness separation logic
• On algebra of program correctness and incorrectness
• Analyzing Program Analyses
• A Coalgebraic Decision Procedure for NetKAT
• Complete Abstractions Everywhere
• A fast compiler for NetKAT
• Equational Theories of Abnormal Termination Based on Kleene Algebra
• Systematic design of program transformation frameworks by abstract interpretation
• Kleene algebra with domain
• Cantor meets Scott: semantic foundations for probabilistic networks
• Making abstract interpretations complete
• NetKAT
• An axiomatic basis for computer programming
• On Hoare logic and Kleene algebra with tests

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