scholarly journals Completeness for a First-Order Abstract Separation Logic

2016 ◽  
pp. 444-463 ◽  
Author(s):  
Zhé Hóu ◽  
Alwen Tiu
Keyword(s):  
Separation Logic ◽  
First Order

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.

scholarly journals Steel: proof-oriented programming in a dependently typed concurrent separation logic

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-30
Author(s):  
Aymeric Fromherz ◽  
Aseem Rastogi ◽  
Nikhil Swamy ◽  
Sydney Gibson ◽  
Guido Martínez ◽  
...  
Keyword(s):  
Linked Data ◽  
Separation Logic ◽  
Concurrent Programs ◽  
Interactive Proof ◽  
First Order ◽  
Session Types ◽  
Verification Condition ◽  
New Formulation ◽  
Concurrent Separation Logic ◽  
Efficient Verification

Steel is a language for developing and proving concurrent programs embedded in F ⋆ , a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F ⋆ , our work focuses on exposing the proof rules of the logic in a form that enables programs and proofs to be effectively co-developed. Our main contributions include a new formulation of a Hoare logic of quintuples involving both separation logic and first-order logic, enabling efficient verification condition (VC) generation and proof discharge using a combination of tactics and SMT solving. We relate the VCs produced by our quintuple system to solving a system of associativity-commutativity (AC) unification constraints and develop tactics to (partially) solve these constraints using AC-matching modulo SMT-dischargeable equations. Our system is fully mechanized and implemented in F ⋆ . We evaluate it by developing several verified programs and libraries, including various sequential and concurrent linked data structures, proof libraries, and a library for 2-party session types. Our experience leads us to conclude that our system enables a mixture of automated and interactive proof, making it productive to build programs foundationally verified against a highly expressive, state-of-the-art CSL.

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.

First-order separation logic

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

scholarly journals A First-Order Logic with Frames

2020 ◽  
pp. 515-543 ◽  
Author(s):  
Adithya Murali ◽  
Lucas Peña ◽  
Christof Löding ◽  
P. Madhusudan
Keyword(s):  
Data Structures ◽  
Order Logic ◽  
Separation Logic ◽  
First Order Logic ◽  
Program Logic ◽  
First Order ◽  
Proof Rules ◽  
Local Specifications ◽  
Recursive Definitions ◽  
The Universe

AbstractWe propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct $$\textit{Sp}(\cdot )$$ Sp ( · ) that captures the implicit supports of formulas— the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL.

Dual systems for all: Higher-order, role-based relational reasoning as a uniquely derived feature of human cognition

2019 ◽  
Vol 42 ◽  
Author(s):  
Daniel J. Povinelli ◽  
Gabrielle C. Glorioso ◽  
Shannon L. Kuznar ◽  
Mateja Pavlic
Keyword(s):  
Temporal Reasoning ◽  
Higher Order ◽  
Important Case ◽  
Human Cognition ◽  
Relational Reasoning ◽  
Dual Systems ◽  
First Order ◽  
Reasoning System ◽  
Role Based

Abstract Hoerl and McCormack demonstrate that although animals possess a sophisticated temporal updating system, there is no evidence that they also possess a temporal reasoning system. This important case study is directly related to the broader claim that although animals are manifestly capable of first-order (perceptually-based) relational reasoning, they lack the capacity for higher-order, role-based relational reasoning. We argue this distinction applies to all domains of cognition.

Sign in / Sign up

Export Citation Format

Share Document