More Like this

1. Abstraction and subsumption in modular verification of C programs

   https://doi.org/10.1007/978-3-030-30942-8_34  

   Beringer, L.; Appel, A (October 2019, 23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods,)

   Representation predicates enable data abstraction in separation logic, but when the same concrete implementation may need to be abstracted in different ways, one needs a notion of subsumption. We demonstrate function-specification subtyping, analogous to subtyping, with a subsumption rule: if ϕ is a of ψ, that is ϕ< : ψ, then x: ϕ implies x: ψ, meaning that any function satisfying specification ϕ can be used wherever a function satisfying ψ is demanded. We extend previous notions of Hoare-logic sub-specification, which already included parameter adaption, to include framing (necessary for separation logic) and impredicative bifunctors (necessary for higher-order functions, i.e. function pointers). We show intersection specifications, with the expected relation to subtyping. We show how this enables compositional modular verification of the functional correctness of C programs, in Coq, with foundational machine-checked proofs of soundness. 

   more » « less
2. Abstraction and subsumption in modular verification of C programs

   https://doi.org/10.1007/s10703-020-00353-1  

   Beringer, Lennart; Appel, Andrew W. (March 2021, Formal Methods in System Design)

   null (Ed.)

   The type-theoretic notions of existential abstraction, subtyping, subsumption, and intersection have useful analogues in separation-logic proofs of imperative programs. We have implemented these as an enhancement of the verified software toolchain (VST). VST is an impredicative concurrent separation logic for the C language, implemented in the Coq proof assistant, and proved sound in Coq. For machine-checked functional-correctness verification of software at scale, VST embeds its expressive program logic in dependently typed higher-order logic (CiC). Specifications and proofs in the program logic can leverage the expressiveness of CiC—so users can overcome the abstraction gaps that stand in the way of top-to-bottom verification: gaps between source code verification, compilation, and domain-specific reasoning, and between different analysis techniques or formalisms. Until now, VST has supported the specification of a program as a flat collection of function specifications (in higher-order separation logic)—one proves that each function correctly implements its specification, assuming the specifications of the functions it calls. But what if a function has more than one specification? In this work, we exploit type-theoretic concepts to structure specification interfaces for C code. This brings modularity principles of modern software engineering to concrete program verification. Previous work used representation predicates to enable data abstraction in separation logic. We go further, introducing function-specification subsumption and intersection specifications to organize the multiple specifications that a function is typically associated with. As in type theory, if 𝜙 is a of 𝜓, that is 𝜙<:𝜓, then 𝑥:𝜙 implies 𝑥:𝜓, meaning that any function satisfying specification 𝜙 can be used wherever a function satisfying 𝜓 is demanded. Subsumption incorporates separation-logic framing and parameter adaptation, as well as step-indexing and specifications constructed via mixed-variance functors (needed for C’s function pointers). 

   more » « less
3. Verified Software Units

   https://doi.org/10.1007/978-3-030-72019-3_5  

   Beringer, Lennart (March 2021, Programming Languages and Systems. ESOP 2021.)

   Yoshida, Nobuko (Ed.)

   Modularity - the partitioning of software into units of functionality that interact with each other via interfaces - has been the mainstay of software development for half a century. In case of the C language, the main mechanism for modularity is the compilation unit / header file abstraction. This paper complements programmatic modularity for C with modularity idioms for specification and verification in the context of Verifiable C, an expressive separation logic for CompCert Clight. Technical innovations include (i) abstract predicate declarations – existential packages that combine Parkinson & Bierman’s abstract predicates with their client-visible reasoning principles; (ii) residual predicates, which help enforcing data abstraction in callback-rich code; and (iii) an application to pure (Smalltalk-style) objects that connects code verification to model-level reasoning about features such as subtyping, self, inheritance, and late binding. We introduce our techniques using concrete example modules that have all been verified using the Coq proof assistant and combine to fully linked verified programs using a novel, abstraction-respecting component composition rule for Verifiable C. 

   more » « less
4. Arithmetizing Shape Analysis

   https://doi.org/10.1007/978-3-031-98668-0_3  

   Wolff, Sebastian; Gupta, Ekanshdeep; Esen, Zafer; Hojjat, Hossein; Rümmer, Philipp; Wies, Thomas (July 2025, Springer Nature Switzerland)

   Abstract Memory safety is a fundamental correctness property of software. For programs that manipulate linked, heap-allocated data structures, ensuring memory safety requires analyzing their possible shapes. Despite significant advances in shape analysis, existing techniques rely on hand-crafted domains tailored to specific data structures, making them difficult to generalize and extend. This paper presents a novel approach that reduces memory-safety proofs to the verification of heap-less imperative programs, enabling the use of off-the-shelf software verification tools. We achieve this reduction through two complementary program instrumentation techniques: space invariants, which enable symbolic reasoning about unbounded heaps, and flow abstraction, which encodes global heap properties as local flow equations. The approach effectively verifies memory safety across a broad range of programs, including concurrent lists and trees that lie beyond the reach of existing shape analysis tools. 

   more » « less
5. Structural temporal logic for mechanized program verification

   Ioannidis, Eleftherios; Zakowski, Yannick; Zdancewic, Steve; Angel, Sebastian (October 2025, Proceedings of the ACM on programming languages)

   Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of models such as traces and automata. Reasoning happens at a very low-level, requiring complex nested (co-)inductive proof techniques and familiarity with proof assistant mechanics (e.g., the guardedness checker). Further, reasoning at the level of models instead of program constructs creates a verification gap that loses the benefits of modularity and composition enjoyed by structural program logics such as Hoare Logic. To address this verification gap, and the lack of compositional proof techniques for temporal specifications, we propose Ticl, a new structural temporal logic. Using Ticl, we encode complex (co-)inductive proof techniques as structural lemmas and focus our reasoning on variants and invariants. We show that it is possible to perform compositional proofs of general temporal properties in a proof assistant, while working at a high level of abstraction. We demonstrate the benefits of Ticl by giving mechanized proofs of safety and liveness properties for programs with scheduling, concurrent shared memory, and distributed consensus, demonstrating a low proof-to-code ratio. 

   more » « less