Separation logic and logics with team semantics

2021 ◽  
pp. 103063
Author(s):  
Darion Haase ◽  
Erich Grädel ◽  
Richard Wilke
Keyword(s):  
Separation Logic ◽  
Team Semantics

scholarly journals Linear capabilities for fully abstract compilation of separation-logic-verified code

2021 ◽  
Vol 31 ◽  
Author(s):  
THOMAS VAN STRYDONCK ◽  
FRANK PIESSENS ◽  
DOMINIQUE DEVRIESE
Keyword(s):  
Spatial Separation ◽  
Separation Logic ◽  
Target Language ◽  
Fine Grained ◽  
Dynamic Contract ◽  
Modular Verification ◽  
Source Program ◽  
Memory Accesses ◽  
Memory Resources ◽  
Efficient Memory

Abstract Separation logic is a powerful program logic for the static modular verification of imperative programs. However, dynamic checking of separation logic contracts on the boundaries between verified and untrusted modules is hard because it requires one to enforce (among other things) that outcalls from a verified to an untrusted module do not access memory resources currently owned by the verified module. This paper proposes an approach to dynamic contract checking by relying on support for capabilities, a well-studied form of unforgeable memory pointers that enables fine-grained, efficient memory access control. More specifically, we rely on a form of capabilities called linear capabilities for which the hardware enforces that they cannot be copied. We formalize our approach as a fully abstract compiler from a statically verified source language to an unverified target language with support for linear capabilities. The key insight behind our compiler is that memory resources described by spatial separation logic predicates can be represented at run time by linear capabilities. The compiler is separation-logic-proof-directed: it uses the separation logic proof of the source program to determine how memory accesses in the source program should be compiled to linear capability accesses in the target program. The full abstraction property of the compiler essentially guarantees that compiled verified modules can interact with untrusted target language modules as if they were compiled from verified code as well. This article is an extended version of one that was presented at ICFP 2019 (Van Strydonck et al., 2019).

scholarly journals Cosmo: a concurrent separation logic for multicore OCaml

2020 ◽  
Vol 4 (ICFP) ◽  
pp. 1-29
Author(s):  
Glen Mével ◽  
Jacques-Henri Jourdan ◽  
François Pottier
Keyword(s):  
Separation Logic ◽  
Concurrent Separation Logic

scholarly journals Distributed causal memory: modular specification and verification in higher-order distributed separation logic

2021 ◽  
Vol 5 (POPL) ◽  
pp. 1-29
Author(s):  
Léon Gondelman ◽  
Simon Oddershede Gregersen ◽  
Abel Nieto ◽  
Amin Timany ◽  
Lars Birkedal
Keyword(s):  
Higher Order ◽  
Separation Logic ◽  
Specification And Verification

scholarly journals The future is ours: prophecy variables in separation logic

2020 ◽  
Vol 4 (POPL) ◽  
pp. 1-32 ◽  
Author(s):  
Ralf Jung ◽  
Rodolphe Lepigre ◽  
Gaurav Parthasarathy ◽  
Marianna Rapoport ◽  
Amin Timany ◽  
...  
Keyword(s):  
Separation Logic ◽  
The Future

scholarly journals QUANTUM TEAM LOGIC AND BELL’S INEQUALITIES

2015 ◽  
Vol 8 (4) ◽  
pp. 722-742 ◽  
Author(s):  
TAPANI HYTTINEN ◽  
GIANLUCA PAOLINI ◽  
JOUKO VÄÄNÄNEN
Keyword(s):  
Quantum Mechanics ◽  
Completeness Theorem ◽  
Probability Logic ◽  
Bell’S Inequalities ◽  
Dependence Logic ◽  
Logical Approach ◽  
Team Semantics ◽  
Bell's Inequalities

AbstractA logical approach to Bell’s Inequalities of quantum mechanics has been introduced by Abramsky and Hardy (Abramsky & Hardy, 2012). We point out that the logical Bell’s Inequalities of Abramsky & Hardy (2012) are provable in the probability logic of Fagin, Halpern and Megiddo (Fagin et al., 1990). Since it is now considered empirically established that quantum mechanics violates Bell’s Inequalities, we introduce a modified probability logic, that we call quantum team logic, in which Bell’s Inequalities are not provable, and prove a Completeness theorem for this logic. For this end we generalise the team semantics of dependence logic (Väänänen, 2007) first to probabilistic team semantics, and then to what we call quantum team semantics.

Sign in / Sign up

Export Citation Format

Share Document