Modular specification and verification of closures in Rust

Closures are a language feature supported by many mainstream languages, combining the ability to package up references to code blocks with the possibility of capturing state from the environment of the closure's declaration. Closures are powerful, but complicate understanding and formal reasoning, especially when closure invocations may mutate objects reachable from the captured state or from closure arguments. This paper presents a novel technique for the modular specification and verification of closure-manipulating code in Rust. Our technique combines Rust's type system guarantees and novel specification features to enable formal verification of rich functional properties. It encodes higher-order concerns into a first-order logic, which enables automation via SMT solvers. Our technique is implemented as an extension of the deductive verifier Prusti, with which we have successfully verified many common idioms of closure usage.

Download Full-text

Summing up Smart Transitions

Computer Aided Verification - Lecture Notes in Computer Science ◽

10.1007/978-3-030-81685-8_15 ◽

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.

Download Full-text

“Most of” leads to undecidability: Failure of adding frequencies to LTL

Lecture Notes in Computer Science - Foundations of Software Science and Computation Structures ◽

10.1007/978-3-030-71995-1_5 ◽

2021 ◽

pp. 82-101

Author(s):

Bartosz Bednarczyk ◽

Jakub Michaliszyn

Keyword(s):

Model Checking ◽

Formal Verification ◽

Temporal Logic ◽

Order Logic ◽

First Order Logic ◽

Statistical Reasoning ◽

First Order ◽

High Interest ◽

The Past ◽

Influence Networks

AbstractLinear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that $$\sigma $$ σ is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and discuss how the undecidability results transfer to first-order logic on words.

Download Full-text

An Overview of VV&A Methods for Conceptual Model

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.444-445.860 ◽

2013 ◽

Vol 444-445 ◽

pp. 860-864

Author(s):

Xiao Jian Ding ◽

Feng Xin Sun

Keyword(s):

Petri Nets ◽

Formal Verification ◽

Conceptual Model ◽

Conceptual Modeling ◽

Order Logic ◽

Model Verification ◽

First Order Logic ◽

Verification Method ◽

First Order ◽

Formal Techniques

This paper summarizes the literature and presents important concepts related to conceptual model verification. Different approaches have been proposed in the literature. These approaches have been introduced as two parts with emphasis on formal techniques. First order logic for structural views and Petri nets for behavioral views are investigated in the search of a practical verification method for conceptual modeling in UML. Then a short assessment of formal verification work for UML will be presented.

Download Full-text

An object-oriented calculus with term constraints

Journal of Functional Programming ◽

10.1017/s0956796806006174 ◽

2007 ◽

Vol 17 (3) ◽

pp. 353-386

Author(s):

GÁBOR M. SURÁNYI

Keyword(s):

Type System ◽

Object Oriented ◽

Order Logic ◽

First Order Logic ◽

Engineering Process ◽

Type Safety ◽

First Order ◽

Multiple Dispatch ◽

Fundamental Requirement ◽

Distinguished Object

AbstractSafety has become a fundamental requirement in all aspects of computer systems. Object-oriented calculi, such as Castagna's λ&-calculus and its variants (Castagna, 1997) ensure type safety in environments based on the distinguished object-oriented paradigm. Although for safety reasons object invariance and operation specifications are getting widely employed in all stages of the engineering process, they are not supported by these calculi. In this paper, a new calculus is presented which supports term (value) constraints besides the key object-oriented mechanisms (class types, inheritance, overloading with multiple dispatch and late binding). We also show how a type with constraints may realise a role, another useful object-oriented modelling element. The soundness of the type system and the confluence of the notion of reduction of the calculus are considered. The contribution also discusses computability issues partially arising from the use of first-order logic to formalise the constraints.

Download Full-text

Using Vampire in Soundness Proofs of Type Systems

10.29007/22x6 ◽

2018 ◽

Author(s):

Sylvia Grewe ◽

Sebastian Erdweg ◽

Mira Mezini

Keyword(s):

Programming Languages ◽

Type System ◽

Lambda Calculus ◽

Type Systems ◽

Current Approach ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Domain Specific ◽

Automated Proof

Type systems for programming languages shall detect type errors in programs before runtime. To ensure that a type system meets this requirement, its soundness must be formally verified. We aim at automating soundness proofs of type systems to facilitate the development of sound type systems for domain-specific languages.Soundness proofs for type systems typically require induction. However, many of the proofs of individual induction cases only require first-order reasoning. For the development of our workbench Veritas, we build on this observation by combining automated first-order theorem provers such as Vampire with automated proof strategies specific to type systems. In this paper, we describe how we encode type soundness proofs in first-order logic using TPTP. We show how we use Vampire to prove the soundness of type systems for the simply-typed lambda calculus and for parts of a typed SQL. We report on which parts of the proofs are handled well by Vampire, and what parts work less well with our current approach.

Download Full-text

Embedding First-order Logic in a Pure Type System with Parameters

Journal of Logic and Computation ◽

10.1093/logcom/11.4.545 ◽

2001 ◽

Vol 11 (4) ◽

pp. 545-557 ◽

Cited By ~ 1

Author(s):

T. Laan

Keyword(s):

Type System ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Pure Type

Download Full-text

First-Order Logic Reasoning Support for the Semantic Web

Journal of Software ◽

10.3724/sp.j.1001.2008.03091 ◽

2009 ◽

Vol 19 (12) ◽

pp. 3091-3099 ◽

Cited By ~ 1

Author(s):

Gui-Hong XU ◽

Jian ZHANG

Keyword(s):

Semantic Web ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Logic Reasoning

Download Full-text

Boolean-valued structures

10.1093/oso/9780198790396.003.0013 ◽

2018 ◽

Author(s):

Tim Button ◽

Sean Walsh

Keyword(s):

Model Theory ◽

Order Logic ◽

First Order Logic ◽

Inference Rules ◽

Mathematical Concepts ◽

Semantic Framework ◽

First Order ◽

Standard Models ◽

Boolean Valued Model ◽

Semantic Values

Chapters 6-12 are driven by questions about the ability to pin down mathematical entities and to articulate mathematical concepts. This chapter is driven by similar questions about the ability to pin down the semantic frameworks of language. It transpires that there are not just non-standard models, but non-standard ways of doing model theory itself. In more detail: whilst we normally outline a two-valued semantics which makes sentences True or False in a model, the inference rules for first-order logic are compatible with a four-valued semantics; or a semantics with countably many values; or what-have-you. The appropriate level of generality here is that of a Boolean-valued model, which we introduce. And the plurality of possible semantic values gives rise to perhaps the ‘deepest’ level of indeterminacy questions: How can humans pin down the semantic framework for their languages? We consider three different ways for inferentialists to respond to this question.

Download Full-text

GAMES AND CARDINALITIES IN INQUISITIVE FIRST-ORDER LOGIC

The Review of Symbolic Logic ◽

10.1017/s1755020321000198 ◽

2021 ◽

pp. 1-28

Author(s):

IVANO CIARDELLI ◽

GIANLUCA GRILLETTI

Keyword(s):

Order Logic ◽

First Order Logic ◽

First Order

Download Full-text

Extensions in graph normal form

Logic Journal of IGPL ◽

10.1093/jigpal/jzaa054 ◽

2020 ◽

Author(s):

Michał Walicki

Keyword(s):

Normal Form ◽

Fixed Points ◽

Propositional Logic ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Special Cases

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.

Download Full-text