Abstraction and subsumption in modular verification of C programs

DOI10.1007/s10703-020-00353-1zbMath1505.68023OpenAlexW3138908006MaRDI QIDQ2147702

Lennart Beringer, Andrew W. Appel

Publication date: 20 June 2022

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-020-00353-1

zbMATH Keywords

foundational program verificationintersection specificationsseparation 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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Efficient extensional binary tries

Uses Software

• Coq
• Dafny
• ACSL
• Frama-C
• VCC
• VeriFast
• Toolchain
• GitHub
• VST-Floyd
• Rust
• RustBelt

Cites Work

• Unnamed Item
• 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
• Dafny: An Automatic Program Verifier for Functional Correctness
• Dynamic Frames in Java Dynamic Logic
• 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