Abstraction and subsumption in modular verification of C programs

DOI10.1007/978-3-030-30942-8_34zbMath1539.68051MaRDI QIDQ6535970

Andrew W. Appel, Lennart Beringer

Publication date: 14 March 2024

zbMATH Keywords

foundational program verificationseparation logicsspecification subsumption

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Solving reflexive domain equations in a category of complete metric spaces
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Hoare logic and auxiliary variables
• A proof outline logic for object-oriented programming
• Relational Decomposition
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Separation logic and abstraction
• Program Logics for Certified Compilers

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