Sound Modular Verification of C Code Executing in an Unverified Context

DOI10.1145/2676726.2676972zbMath1345.68089OpenAlexW2152178634MaRDI QIDQ2819844

Pieter Agten, Bart Jacobs, Frank Piessens

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

verificationseparation logicruntime checking

Mathematics Subject Classification ID

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

Related Items (1)

Linear capabilities for fully abstract compilation of separation-logic-verified code

This page was built for publication: Sound Modular Verification of C Code Executing in an Unverified Context