Abstraction and subsumption in modular verification of C programs

DOI10.1007/S10703-020-00353-1zbMATH Open1505.68023OpenAlexW3138908006MaRDI QIDQ2147702FDOQ2147702

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)

Cites Work

• Dafny: An Automatic Program Verifier for Functional Correctness
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Types and programing languages
• Solving reflexive domain equations in a category of complete metric spaces
• Separation logic and abstraction
• A proof outline logic for object-oriented programming
• Hoare logic and auxiliary variables
• Relational Decomposition
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Program Logics for Certified Compilers
• Dynamic Frames in Java Dynamic Logic
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (3)

• Bridging the Gap: Automatic Verified Abstraction of C
• Efficient extensional binary tries
• Modular inference of subprogram contracts for safety checking

Uses Software

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

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)