# Abstraction and subsumption in modular verification of C programs

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

To refer to this page use: http://arks.princeton.edu/ark:/88435/pr14r8r
DC FieldValueLanguage
dc.contributor.authorBeringer, Lennart-
dc.contributor.authorAppel, Andrew W-
dc.date.accessioned2021-10-08T19:51:05Z-
dc.date.available2021-10-08T19:51:05Z-
dc.date.issued2021en_US
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.identifier.issn1572-8102-
dc.identifier.urihttps://www.cs.princeton.edu/~eberinge/funspec_sub.pdf-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr14r8r-
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.language.isoen_USen_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
dc.identifier.doi10.1007/s10703-020-00353-1-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/journal-articleen_US

Files in This Item:
File Description SizeFormat