scholarly journals Connecting Higher-Order Separation Logic to a First-Order Outside World

2020 ◽  
pp. 428-455 ◽  
Author(s):  
William Mansky ◽  
Wolf Honoré ◽  
Andrew W. Appel
Keyword(s):  
Program Verification ◽  
Higher Order ◽  
Separation Logic ◽  
C Programs ◽  
First Order ◽  
System Calls ◽  
Correctness Of Programs ◽  
Verified Software ◽  
Order State ◽  
Order Separation

AbstractSeparation logic is a useful tool for proving the correctness of programs that manipulate memory, especially when the model of memory includes higher-order state: Step-indexing, predicates in the heap, and higher-order ghost state have been used to reason about function pointers, data structure invariants, and complex concurrency patterns. On the other hand, the behavior of system features (e.g., operating systems) and the external world (e.g., communication between components) is usually specified using first-order formalisms. In principle, the soundness theorem of a separation logic is its interface with first-order theorems, but the soundness theorem may implicitly make assumptions about how other components are specified, limiting its use. In this paper, we show how to extend the higher-order separation logic of the Verified Software Toolchain to interface with a first-order verified operating system, in this case CertiKOS, that mediates its interaction with the outside world. The resulting system allows us to prove the correctness of C programs in separation logic based on the semantics of system calls implemented in CertiKOS. It also demonstrates that the combination of interaction trees + CompCert memories serves well as a lingua franca to interface and compose two quite different styles of program verification.

Higher order separation logic

2014 ◽  
pp. 75-75
Author(s):  
Andrew W. Appel ◽  
Robert Dockins ◽  
Aquinas Hobor ◽  
Lennart Beringer ◽  
Josiah Dodds ◽  
...  
Keyword(s):  
Higher Order ◽  
Separation Logic ◽  
Order Separation

scholarly journals Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic

2016 ◽  
Vol 38 (2) ◽  
pp. 1-72 ◽  
Author(s):  
Mike Dodds ◽  
Suresh Jagannathan ◽  
Matthew J. Parkinson ◽  
Kasper Svendsen ◽  
Lars Birkedal
Keyword(s):  
Higher Order ◽  
Separation Logic ◽  
Order Separation

Applying higher-order separation logic

2014 ◽  
pp. 130-133
Author(s):  
Andrew W. Appel ◽  
Robert Dockins ◽  
Aquinas Hobor ◽  
Lennart Beringer ◽  
Josiah Dodds ◽  
...  
Keyword(s):  
Higher Order ◽  
Separation Logic ◽  
Order Separation

scholarly journals Certifying the synthesis of heap-manipulating programs

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-29
Author(s):  
Yasunari Watanabe ◽  
Kiran Gopinathan ◽  
George Pîrlea ◽  
Nadia Polikarpova ◽  
Ilya Sergey
Keyword(s):  
Program Verification ◽  
Ad Hoc ◽  
Program Synthesis ◽  
Separation Logic ◽  
Third Party ◽  
Correctness Proofs ◽  
Deductive Synthesis ◽  
Efficient Machine ◽  
Verified Software ◽  
Executable Programs

Automated deductive program synthesis promises to generate executable programs from concise specifications, along with proofs of correctness that can be independently verified using third-party tools. However, an attempt to exercise this promise using existing proof-certification frameworks reveals significant discrepancies in how proof derivations are structured for two different purposes: program synthesis and program verification. These discrepancies make it difficult to use certified verifiers to validate synthesis results, forcing one to write an ad-hoc translation procedure from synthesis proofs to correctness proofs for each verification backend. In this work, we address this challenge in the context of the synthesis and verification of heap-manipulating programs. We present a technique for principled translation of deductive synthesis derivations (a.k.a. source proofs) into deductive target proofs about the synthesised programs in the logics of interactive program verifiers. We showcase our technique by implementing three different certifiers for programs generated via SuSLik, a Separation Logic-based tool for automated synthesis of programs with pointers, in foundational verification frameworks embedded in Coq: Hoare Type Theory (HTT), Iris, and Verified Software Toolchain (VST), producing concise and efficient machine-checkable proofs for characteristic synthesis benchmarks.

scholarly journals The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic

2021 ◽  
Vol 22 (2) ◽  
pp. 1-56
Author(s):  
Stéphane Demri ◽  
Etienne Lozes ◽  
Alessio Mansutti
Keyword(s):  
Natural Extension ◽  
Point Of View ◽  
Separation Logic ◽  
Polynomial Space ◽  
Full Extension ◽  
Computational Point ◽  
First Order ◽  
Verification Tools ◽  
Memory States ◽  
Order Separation

The list segment predicate ls used in separation logic for verifying programs with pointers is well suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and verification tools start to handle the magic wand connective. This is a very natural extension that has not been studied so far. We show that the restriction without the separating implication can be solved in polynomial space by using an appropriate abstraction for memory states, whereas the full extension is shown undecidable by reduction from first-order separation logic. Many variants of the logic and fragments are also investigated from the computational point of view when ls is added, providing numerous results about adding reachability predicates to quantifier-free separation logic.

Sign in / Sign up

Export Citation Format

Share Document