Global invariants for analysing multi-threaded applications

2003 ◽  
Vol 52 (4) ◽  
pp. 413
Author(s):  
M Müller-Olm ◽  
H Seidl ◽  
V Vene
Keyword(s):  
Global Invariants

scholarly journals Direct perception of global invariants is not a fruitful notion

2001 ◽  
Vol 24 (2) ◽  
pp. 235-235
Author(s):  
C. (Lieke) E. Peper ◽  
Peter J. Beek
Keyword(s):  
Ecological Perspective ◽  
Direct Perception ◽  
Sources Of Information ◽  
Sensory Signals ◽  
Global Invariants ◽  
Behavioral Evidence

The epistemological premises and scientific viability of Stoffregen & Bardy's ecological perspective are evaluated by analyzing the concept of direct perception of global invariants vis-à-vis (1) behavioral evidence that perception is based on the integration of modal sources of information and (2) neurophysiological aspects of the integration of sensory signals.

Energy principle with global invariants: Applications

1983 ◽  
Vol 26 (2) ◽  
pp. 526 ◽  
Author(s):  
A. Bhattacharjee
Keyword(s):  
Energy Principle ◽  
Global Invariants

scholarly journals Summing up Smart Transitions

2021 ◽  
pp. 317-340
Author(s):  
Neta Elad ◽  
Sophie Rain ◽  
Neil Immerman ◽  
Laura Kovács ◽  
Mooly Sagiv
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Smart Contracts ◽  
Automate Reasoning ◽  
Arbitrary Length ◽  
First Order ◽  
Smt Solvers ◽  
Transfer Operation ◽  
Global Invariants ◽  
High Level

AbstractSome of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer programs that operate over them, e.g., in Solidity. The ability to reason about sums is essential: even the simplest ERC-20 token standard of the Ethereum community provides a way to access the total supply of balances.Unfortunately, reasoning about code written against this interface is non-trivial: the number of addresses is unbounded, and establishing global invariants like the preservation of the sum of the balances by operations like transfer requires higher-order reasoning. In particular, automated reasoners do not provide ways to specify summations of arbitrary length.In this paper, we present a generalization of first-order logic which can express the unbounded sum of balances. We prove the decidablity of one of our extensions and the undecidability of a slightly richer one. We introduce first-order encodings to automate reasoning over software transitions with summations. We demonstrate the applicability of our results by using SMT solvers and first-order provers for validating the correctness of common transitions in smart contracts.

scholarly journals Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints

2021 ◽  
pp. 438-442
Author(s):  
Simmo Saan ◽  
Michael Schwarz ◽  
Kalmer Apinis ◽  
Julian Erhard ◽  
Helmut Seidl ◽  
...  
Keyword(s):  
Static Analysis ◽  
Abstract Interpretation ◽  
Analysis Framework ◽  
Data Race ◽  
C Programs ◽  
Global Invariants ◽  
Race Analysis

AbstractGoblintis a static analysis framework for C programs specializing in data race analysis. It relies on thread-modular abstract interpretation where thread interferences are accounted for by means of flow-insensitive global invariants.

scholarly journals Conformal geometry and global invariants

1991 ◽  
Vol 1 (3) ◽  
pp. 279-308 ◽  
Author(s):  
Thomas P. Branson ◽  
Bent Ørsted
Keyword(s):  
Conformal Geometry ◽  
Global Invariants

Local Reasoning for Global Invariants, Part II

2013 ◽  
Vol 60 (3) ◽  
pp. 1-73 ◽  
Author(s):  
Anindya Banerjee ◽  
David A. Naumann
Keyword(s):  
Local Reasoning ◽  
Global Invariants
Sign in / Sign up

Export Citation Format

Share Document