Abstraction and subsumption in modular verification of C programs

DOI10.1007/978-3-030-30942-8_34MaRDI QIDQ6535970zbMATH OpenFDO

Authors Lennart Beringer, Andrew W. Appel

Publication date 14 March 2024

zbMATH Keywords

foundational program verificationseparation logicsspecification subsumption

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Abstraction and subsumption in modular verification of C programs
• Separation logic and abstraction
• Verified software units
• Two for the price of one: lifting separation logic assertions
• Abstracting Allocation

Cites work

• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• A proof outline logic for object-oriented programming
• Hoare logic and auxiliary variables
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Program logics for certified compilers
• Relational decomposition
• Separation logic and abstraction
• Solving reflexive domain equations in a category of complete metric spaces
• Types and programing languages
• VST-Floyd: a separation logic tool to verify correctness of C programs

This page was built for publication: Abstraction and subsumption in modular verification of C programs

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