Sound modular verification of C code executing in an unverified context

DOI10.1145/2676726.2676972MaRDI QIDQ2819844zbMATH OpenOpenAlexFDO

Authors Pieter Agten, Frank Piessens, Bart Jacobs

Publication date 29 September 2016

Published in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://lirias.kuleuven.be/handle/123456789/471365

zbMATH Keywords

runtime checkingseparation logicverification

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Linear capabilities for fully abstract compilation of separation-logic-verified code
• Verified software units
• Sufficient Preconditions for Modular Assertion Checking
• Modular software fault isolation as abstract interpretation
• Formal verification of C systems code. Structured types, separation logic and theorem proving

Cited in

(4)

• Verified software units
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• Sufficient Preconditions for Modular Assertion Checking
• Verified runtime assertion checking for memory properties

This page was built for publication: Sound modular verification of C code executing in an unverified context

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