A correctness and incorrectness program logic

DOI10.1145/3582267MaRDI QIDQ7032172zbMATH OpenFDO

Authors Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Francesco Ranzato

Publication date 5 February 2025

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3582267

zbMATH Keywords

abstract interpretationprogram verificationprogram analysisprogram logiclocal completenessabstract domainincorrectness logicbest correct approximation

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 1222407 (Why is no real title available?)
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• scientific article; zbMATH DE number 1956470 (Why is no real title available?)
• scientific article; zbMATH DE number 7559486 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3421895 (Why is no real title available?)
• Abstract Interpretation Frameworks
• Algebras of modal operators and partial correctness
• An axiomatic basis for computer programming
• Analyzing program analyses
• Classes of Recursively Enumerable Sets and Their Decision Problems
• Code obfuscation against abstract model checking attacks
• Constructive versions of Tarski's fixed point theorems
• Continuous reasoning: scaling the impact of formal methods
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Grammar Analysis and Parsing by Abstract Interpretation
• Incorrectness logic for graph programs
• Limits and difficulties in the design of under-approximation abstract domains
• Local completeness logic on Kleene algebra with tests
• Local reasoning about the presence of bugs: incorrectness separation logic
• Making abstract domains condensing
• Making abstract interpretations complete
• Monadic second-order incorrectness logic for GP 2
• On algebra of program correctness and incorrectness
• Optimal domains for disjunctive abstract interpretation
• Principles of abstract interpretation
• Program analysis is harder than verification: a computability perspective
• Reverse Hoare logic
• The octagon abstract domain
• Tools and Algorithms for the Construction and Analysis of Systems
• Types and programing languages
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• Broadening the applicability of local completeness analysis with intensional and extensional guarantees

This page was built for publication: A correctness and incorrectness program logic

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