local reasoning
Recently Published Documents


TOTAL DOCUMENTS

56
(FIVE YEARS 14)

H-INDEX

11
(FIVE YEARS 1)

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-27
Author(s):  
Xuan-Bach Le ◽  
Shang-Wei Lin ◽  
Jun Sun ◽  
David Sanan

It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including Deutsch–Jozsa’s algorithm and Grover's algorithm.


Author(s):  
Zhao Jin ◽  
Bowen Zhang ◽  
Lei Zhang ◽  
Yongzhi Cao ◽  
Hanpin Wang

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-26
Author(s):  
Pengbo Yan ◽  
Toby Murray

We present Security Relaxed Separation Logic (SecRSL), a separation logic for proving information-flow security of C11 programs in the Release-Acquire fragment with relaxed accesses. SecRSL is the first security logic that (1) supports weak-memory reasoning about programs in a high-level language; (2) inherits separation logic’s virtues of compositional, local reasoning about (3) expressive security policies like value-dependent classification. SecRSL is also, to our knowledge, the first security logic developed over an axiomatic memory model. Thus we also present the first definitions of information-flow security for an axiomatic weak memory model, against which we prove SecRSL sound. SecRSL ensures that programs satisfy a constant-time security guarantee, while being free of undefined behaviour. We apply SecRSL to implement and verify the functional correctness and constant-time security of a range of concurrency primitives, including a spinlock module, a mixed-sensitivity mutex, and multiple synchronous channel implementations. Empirical performance evaluations of the latter demonstrate SecRSL’s power to support the development of secure and performant concurrent C programs.


2021 ◽  
Author(s):  
Thomas Ågotnes ◽  
Yì N. Wáng

Several different notions of group knowledge have been extensively studied in the epistemic and doxastic logic literature, including common knowledge, general knowledge (everybody-knows) and distributed knowledge. In this paper we study a natural notion of group knowledge between general and distributed knowledge: somebody-knows. While something is general knowledge if and only if it is known by everyone, this notion holds if and only if it is known by someone. This is stronger than distributed knowledge, which is the knowledge that follows from the total knowledge in the group. We introduce a modality for somebody-knows in the style of standard group knowledge modalities, and study its properties. Unlike the other mentioned group knowledge modalities, somebody-knows is not a normal modality; in particular it lacks the conjunctive closure property. We provide an equivalent neighbourhood semantics for the language with a single somebody-knows modality, together with a completeness result: the somebody-knows modalities are completely characterised by the modal logic EMN extended with a particular weak conjunctive closure axiom. We also show that the satisfiability problem for this logic is PSPACE-complete. The neighbourhood semantics and the completeness and complexity results also carry over to logics for so-called local reasoning (Fagin et al. 1995) with bounded ``frames of mind'', correcting an existing completeness result in the literature (Allen 2005).


Author(s):  
Samera Ibrahim Kadum Al-Addal

Innovation has two key levers: the capacity to consider and predict consumer desires, on the one hand, and the building of collaboration between the economic environment, metropolitan players, and knowledge and development actors, somewhere else. Innovation is not just technical, and it disrupts traditions and station partners' aspirations and perceptions: planners, administrators, consumers or clients, and causes a change in locations and uses. The expansion of the rail network in Iraq is renewing station sites, especially in Iraq, which, at the cost of medium-sized cities between these cities, prefer the logic of productivity-focused on express services between major cities. On the field, this alternative translates into two styles of stations that are central base stations for significant towns, and medium- and small-town terminals—establishing stations benefits from an interconnected phase of all spatial organization types. Suppose we research the decision phase that led to the establishment of train stations in Iraq. In that case, we find that this option and construction strategies are a mixture of component elements according to the area details served and actors' strategies. Most chosen sites result from deep relationships between global, regional, and local reasoning.


2021 ◽  
pp. 58-72
Author(s):  
Yifeng Ding ◽  
Jixin Liu ◽  
Yanjing Wang
Keyword(s):  

Author(s):  
Fabio Papacchini ◽  
Cláudia Nalon ◽  
Ullrich Hustadt ◽  
Clare Dixon

AbstractWe present novel reductions of the propositional modal logics "Image missing" , "Image missing" , "Image missing" , "Image missing" and "Image missing" to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover "Image missing" to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover "Image missing" performs well when compared with a specialised resolution calculus for these logics and with the b̆uilt-in reductions of the first-order prover SPASS.


Author(s):  
Azalea Raad ◽  
Josh Berdine ◽  
Hoang-Hai Dang ◽  
Derek Dreyer ◽  
Peter O’Hearn ◽  
...  

Sign in / Sign up

Export Citation Format

Share Document