scholarly journals A Complete Axiomatisation for Quantifier-Free Separation Logic

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Stéphane Demri ◽  
Étienne Lozes ◽  
Alessio Mansutti
Keyword(s):  
Propositional Calculus ◽  
Separation Logic ◽  
Proof System ◽  
Inference Rules ◽  
Bottom Up ◽  
Magic Wand ◽  
Proof Systems ◽  
External Feature

We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into account. Therefore, we present the first internal Hilbert-style axiomatisation for quantifier-free separation logic. The calculus is divided in three parts: the axiomatisation of core formulae where Boolean combinations of core formulae capture the expressivity of the whole logic, axioms and inference rules to simulate a bottom-up elimination of separating connectives, and finally structural axioms and inference rules from propositional calculus and Boolean BI with the magic wand.

Labelled cyclic proofs for separation logic

2021 ◽  
Author(s):  
Didier Galmiche ◽  
Daniel Méry
Keyword(s):  
Data Structures ◽  
Program Verification ◽  
Separation Logic ◽  
Proof System ◽  
Proof Systems ◽  
Verification Tools ◽  
Definition Of ◽  
Logical Formalism

Abstract Separation logic (SL) is a logical formalism for reasoning about programs that use pointers to mutate data structures. It is successful for program verification as an assertion language to state properties about memory heaps using Hoare triples. Most of the proof systems and verification tools for ${\textrm{SL}}$ focus on the decidable but rather restricted symbolic heaps fragment. Moreover, recent proof systems that go beyond symbolic heaps are purely syntactic or labelled systems dedicated to some fragments of ${\textrm{SL}}$ and they mainly allow either the full set of connectives, or the definition of arbitrary inductive predicates, but not both. In this work, we present a labelled proof system, called ${\textrm{G}_{\textrm{SL}}}$, that allows both the definition of cyclic proofs with arbitrary inductive predicates and the full set of SL connectives. We prove its soundness and show that we can derive in ${\textrm{G}_{\textrm{SL}}}$ the built-in rules for data structures of another non-cyclic labelled proof system and also that ${\textrm{G}_{\textrm{SL}}}$ is strictly more powerful than that system.

A proof system for separation logic with magic wand

2014 ◽  
Vol 49 (1) ◽  
pp. 477-490 ◽  
Author(s):  
Wonyeol Lee ◽  
Sungwoo Park
Keyword(s):  
Separation Logic ◽  
Proof System ◽  
Magic Wand

scholarly journals TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

2021 ◽  
Vol 43 (4) ◽  
pp. 1-134
Author(s):  
Emanuele D’Osualdo ◽  
Julian Sutherland ◽  
Azadeh Farzan ◽  
Philippa Gardner
Keyword(s):  
Case Studies ◽  
Separation Logic ◽  
Proof System ◽  
Concurrent Programs ◽  
Semantic Model ◽  
Compositional Reasoning ◽  
Fine Grained ◽  
Fundamental Innovation ◽  
Concurrent Separation Logic

We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking : that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients that use such operations without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. We introduce a novel semantic model using layered subjective obligations to express liveness invariants and a proof system that is sound with respect to the model. The subtlety of our specifications and reasoning is illustrated using several case studies.

scholarly journals A duality between proof systems for cyclic term graphs

2007 ◽  
Vol 17 (3) ◽  
pp. 439-484 ◽  
Author(s):  
CLEMENS GRABMAYER
Keyword(s):  
Close Connection ◽  
Proof System ◽  
Consistency Checking ◽  
Duality Result ◽  
First Order ◽  
Proof Systems ◽  
Similar Proof ◽  
Equational Specifications ◽  
Cyclic Term

This paper presents a proof-theoretic observation about two kinds of proof systems for bisimilarity between cyclic term graphs.First we consider proof systems for demonstrating that μ term specifications of cyclic term graphs have the same tree unwinding. We establish a close connection between adaptations for μ terms over a general first-order signature of the coinductive axiomatisation of recursive type equivalence by Brandt and Henglein (Brandt and Henglein 1998) and of a proof system by Ariola and Klop (Ariola and Klop 1995) for consistency checking. We show that there exists a simple duality by mirroring between derivations in the former system and formalised consistency checks, which are called ‘consistency unfoldings', in the latter. This result sheds additional light on the axiomatisation of Brandt and Henglein: it provides an alternative soundness proof for the adaptation considered here.We then outline an analogous duality result that holds for a pair of similar proof systems for proving that equational specifications of cyclic term graphs are bisimilar.

FUNCTIONAL PEARL Functional chart parsing of context-free grammars

2004 ◽  
Vol 14 (6) ◽  
pp. 669-680
Author(s):  
PETER LJUNGLÖF
Keyword(s):  
Data Structure ◽  
Time Complexity ◽  
Inference Rules ◽  
Global State ◽  
Bottom Up ◽  
Space And Time ◽  
Chart Parsing ◽  
The Many ◽  
Context Free ◽  
Context Free Grammars

This paper implements a simple and elegant version of bottom-up Kilbury chart parsing (Kilbury, 1985; Wirén, 1992). This is one of the many chart parsing variants, which are all based on the data structure of charts. The chart parsing process uses inference rules to add new edges to the chart, and parsing is complete when no further edges can be added. One novel aspect of this implementation is that it doesn't have to rely on a global state for the implementation of the chart. This makes the code clean, elegant and declarative, while still having the same space and time complexity as the standard imperative implementations.

scholarly journals Universal Hash Proofs and a Paradigm for Adaptive Chosen Ciphertext Secure Public-Key Encryption

2001 ◽  
Vol 8 (37) ◽  
Author(s):  
Ronald Cramer ◽  
Victor Shoup
Keyword(s):  
Special Kind ◽  
Public Key ◽  
Proof System ◽  
Reasonable Assumption ◽  
Encryption Scheme ◽  
Public Key Encryption ◽  
Proof Systems ◽  
Encryption Schemes ◽  
Hash Proof System ◽  
Chosen Ciphertext Attack

We present several new and fairly practical public-key encryption schemes and prove them secure against adaptive chosen ciphertext attack. One scheme is based on Paillier's Decision Composite Residuosity (DCR) assumption, while another is based in the classical Quadratic Residuosity (QR) assumption. The analysis is in the standard cryptographic model, i.e., the security of our schemes does not rely on the Random Oracle model.<br /> <br />We also introduce the notion of a universal hash proof system. Essentially, this is a special kind of non-interactive zero-knowledge proof system for an NP language. We do not show that universal hash proof systems exist for all NP languages, but we do show how to construct very efficient universal hash proof systems for a general class of group-theoretic language membership problems.<br /> <br />Given an efficient universal hash proof system for a language with certain natural cryptographic indistinguishability properties, we show how to construct an efficient public-key encryption schemes secure against adaptive chosen ciphertext attack in the standard model. Our construction only uses the universal hash proof system as a primitive: no other primitives are required, although even more efficient encryption schemes can be obtained by using hash functions with appropriate collision-resistance properties. We show how to construct efficient universal hash proof systems for languages related to the DCR and QR assumptions. From these we get corresponding public-key encryption schemes that are secure under these assumptions. We also show that the Cramer-Shoup encryption scheme (which up until now was the only practical encryption scheme that could be proved secure against adaptive chosen ciphertext attack under a reasonable assumption, namely, the Decision Diffie-Hellman assumption) is also a special case of our general theory.

scholarly journals Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding

2009 ◽  
Vol 19 (3) ◽  
pp. 435-500 ◽  
Author(s):  
DOMINIQUE LARCHEY-WENDLING ◽  
DIDIER GALMICHE
Keyword(s):  
Representation Theorem ◽  
Separation Logic ◽  
Semantic Relations ◽  
Proof System ◽  
Kripke Semantics ◽  
Unexpected Result ◽  
Logical Implication ◽  
Logical Basis ◽  
Syntactic Constraints ◽  
Intuitionistic Version

The logic of Bunched Implications, through both its intuitionistic version (BI) and one of its classical versions, called Boolean BI (BBI), serves as a logical basis to spatial or separation logic frameworks. In BI, the logical implication is interpreted intuitionistically whereas it is generally interpreted classically in spatial or separation logics, as in BBI. In this paper, we aim to give some new insights into the semantic relations between BI and BBI. Then we propose a sound and complete syntactic constraints based framework for the Kripke semantics of both BI and BBI, a sound labelled tableau proof system for BBI, and a representation theorem relating the syntactic models of BI to those of BBI. Finally, we deduce as our main, and unexpected, result, a sound and faithful embedding of BI into BBI.

scholarly journals A Deductive Approach towards Reasoning about Algebraic Transition Systems

2015 ◽  
Vol 2015 ◽  
pp. 1-12
Author(s):  
Jun Fu ◽  
Jinzhao Wu ◽  
Hongyan Tan
Keyword(s):  
Complex Systems ◽  
Dynamic Logic ◽  
Decision Procedures ◽  
Proof System ◽  
Search Problem ◽  
Inference Rules ◽  
Algebraic Equations ◽  
Transition Systems ◽  
Proof Search ◽  
Polynomial Ideals

Algebraic transition systems are extended from labeled transition systems by allowing transitions labeled by algebraic equations for modeling more complex systems in detail. We present a deductive approach for specifying and verifying algebraic transition systems. We modify the standard dynamic logic by introducing algebraic equations into modalities. Algebraic transition systems are embedded in modalities of logic formulas which specify properties of algebraic transition systems. The semantics of modalities and formulas is defined with solutions of algebraic equations. A proof system for this logic is constructed to verify properties of algebraic transition systems. The proof system combines with inference rules decision procedures on the theory of polynomial ideals to reduce a proof-search problem to an algebraic computation problem. The proof system proves to be sound but inherently incomplete. Finally, a typical example illustrates that reasoning about algebraic transition systems with our approach is feasible.

Relational proof system for relevant logics

1992 ◽  
Vol 57 (4) ◽  
pp. 1425-1440 ◽  
Author(s):  
Ewa Orlowska
Keyword(s):  
Natural Deduction ◽  
Proof System ◽  
Algebraic Semantics ◽  
Proof Systems ◽  
Relevant Logics ◽  
Deduction Rules

AbstractA method is presented for constructing natural deduction-style systems for propositional relevant logics. The method consists in first translating formulas of relevant logics into ternary relations, and then defining deduction rules for a corresponding logic of ternary relations. Proof systems of that form are given for various relevant logics. A class of algebras of ternary relations is introduced that provides a relation-algebraic semantics for relevant logics.

Sign in / Sign up

Export Citation Format

Share Document