Skip to main content

Abstraction and subsumption in modular verification of C programs

Author(s): Beringer, Lennart; Appel, Andrew W

To refer to this page use:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorBeringer, Lennart-
dc.contributor.authorAppel, Andrew W-
dc.identifier.citationBeringer, Lennart, and Andrew W. Appel. "Abstraction and subsumption in modular verification of C programs." Formal Methods in System Design (2021). doi:10.1007/s10703-020-00353-1en_US
dc.description.abstractThe type-theoretic notions of existential abstraction, subtyping, subsumption, and intersec-tion have useful analogues in separation-logic proofs of imperative programs. We haveimplemented these as an enhancement of the verified software toolchain (VST). VST isan impredicative concurrent separation logic for the C language, implemented in the Coqproof assistant, and proved sound in Coq. For machine-checked functional-correctness veri-fication of software at scale, VST embeds its expressive program logic in dependently typedhigher-order logic (CiC). Specifications and proofs in the program logic can leverage theexpressiveness of CiC—so users can overcome the abstraction gaps that stand in the way oftop-to-bottom verification: gaps between source code verification, compilation, and domain-specific reasoning, and between different analysis techniques or formalisms. Until now, VSThas supported the specification of a program as a flat collection of function specifications (inhigher-order separation logic)—one proves that each function correctly implements its spec-ification, assuming the specifications of the functions it calls. But what if a function has morethan one specification? In this work, we exploit type-theoretic concepts to structure specifica-tion interfaces for C code. This brings modularity principles of modern software engineeringto concrete program verification. Previous work used representation predicates to enabledataabstractionin separation logic. We go further, introducingfunction-specification subsump-tionandintersection specificationsto organize the multiple specifications that a function istypically associated with. As in type theory, ifφis afunspec-subofψ,thatisφ<:ψ,thenx:φimpliesx:ψ, meaning that any function satisfying specificationφcan be usedwherever a function satisfyingψis demanded. Subsumption incorporates separation-logicframing and parameter adaptation, as well as step-indexing and specifications constructedvia mixed-variance functors (needed for C’s function pointers).en_US
dc.relation.ispartofFormal Methods in System Designen_US
dc.rightsAuthor's manuscripten_US
dc.titleAbstraction and subsumption in modular verification of C programsen_US
dc.typeJournal Articleen_US

Files in This Item:
File Description SizeFormat 
AbstractionSubsumption.pdf424.05 kBAdobe PDFView/Download

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.