Abstraction and subsumption in modular verification of C programs

DOI10.1007/S10703-020-00353-1MaRDI QIDQ2147702zbMATH OpenOpenAlexFDO

Authors 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) 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)

Recommendations

• Verified software units
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Separation logic and abstraction
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Proof Abstraction for Imperative Languages

Cites work

• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• A proof outline logic for object-oriented programming
• Dafny: an automatic program verifier for functional correctness
• Dynamic frames in Java dynamic logic
• 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

Cited in

(6)

• Abstraction and subsumption in modular verification of C programs
• Bridging the Gap: Automatic Verified Abstraction of C
• Verified software units
• Efficient extensional binary tries
• Modular inference of subprogram contracts for safety checking
• VST-Floyd: a separation logic tool to verify correctness of C programs

Describes a project that uses

Uses Software

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

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 Q2147702)