Separation logic + superposition calculus = heap theorem prover

Term algebras are important structures in many areas of mathematics and computer science. Reasoning about their theories in superposition-based first-order theorem provers is made difficult by the acyclicity property of terms, which is not finitely axiomatizable. We present an inference rule that extends the superposition calculus and allows reasoning about term algebras without axioms to describe the acyclicity property. We detail an indexing technique to efficiently apply this rule in problems containing a large number of clauses. Finally we experimentally evaluate an implementation of this extended calculus in the first-order theorem prover Vampire. The results show that this technique is able to find proofs for difficult problems that existing SMT solvers and first-order theorem provers are unable to solve.

Download Full-text

A Clausal Normal Form Translation for FOOL

10.29007/ltkk ◽

2018 ◽

Author(s):

Evgenii Kotelnikov ◽

Laura Kovács ◽

Martin Suda ◽

Andrei Voronkov

Keyword(s):

Normal Form ◽

Programming Languages ◽

Program Analysis ◽

State Of The Art ◽

Order Logic ◽

Theorem Prover ◽

First Order Logic ◽

First Order ◽

Theorem Provers ◽

Superposition Calculus

Automated theorem provers for first-order logic usually operate on sets of first-order clauses. It is well-known that the translation of a formula in full first-order logic to a clausal normal form (CNF) can crucially affect performance of a theorem prover. In our recent work we introduced a modification of first-order logic extended by the first class boolean sort and syntactical constructs that mirror features of programming languages. We called this logic FOOL. Formulas in FOOL can be translated to ordinary first-order formulas and checked by first-order theorem provers. While this translation is straightforward, it does not result in a CNF that can be efficiently handled by state-of-the-art theorem provers which use superposition calculus. In this paper we present a new CNF translation algorithm for FOOL that is friendly and efficient for superposition-based first-order provers. We implemented the algorithm in the Vampire theorem prover and evaluated it on a large number of problems coming from formalisation of mathematics and program analysis. Our experimental results show an increase of performance of the prover with our CNF translation compared to the naive translation.

Download Full-text

Polymorphic+Typeclass Superposition

10.29007/8v2f ◽

2018 ◽

Author(s):

Daniel Wand

Keyword(s):

Type System ◽

Theorem Prover ◽

Highly Efficient ◽

Type Classes ◽

Polymorphic Type ◽

Superposition Calculus

We present an extension of superposition that natively handles a polymorphic type system extended with type classes, thus eliminating the need for type encodings when used by an interactive theorem prover like Isabelle/HOL. We describe syntax, typing rules, semantics, the polymorphic superposition calculus and an evaluation on a problem set that is generated from Isabelle/HOL theories. Our evaluation shows that native polymorphic+typeclass performance compares favorably to monomorphisation, a highly efficient but incomplete way of dealing with polymorphism.

Download Full-text

Superposition with First-class Booleans and Inprocessing Clausification

Automated Deduction – CADE 28 - Lecture Notes in Computer Science ◽

10.1007/978-3-030-79876-5_22 ◽

2021 ◽

pp. 378-395

Author(s):

Visa Nummelin ◽

Alexander Bentkamp ◽

Sophie Tourret ◽

Petar Vukmirović

Keyword(s):

State Of The Art ◽

Higher Order ◽

The State ◽

Order Logic ◽

Theorem Prover ◽

First Order Logic ◽

Higher Order Logic ◽

First Order ◽

Superposition Calculus

AbstractWe present a complete superposition calculus for first-order logic with an interpreted Boolean type. Our motivation is to lay the foundation for refutationally complete calculi in more expressive logics with Booleans, such as higher-order logic, and to make superposition work efficiently on problems that would be obfuscated when using clausification as preprocessing. Working directly on formulas, our calculus avoids the costly axiomatic encoding of the theory of Booleans into first-order logic and offers various ways to interleave clausification with other derivation steps. We evaluate our calculus using the Zipperposition theorem prover, and observe that, with no tuning of parameters, our approach is on a par with the state-of-the-art approach.

Download Full-text

Formal Verification of Helicopter Automatic Landing Control Algorithm in Theorem Prover Coq

10.23940/ijpe.18.09.p2.19471957 ◽

2018 ◽

Cited By ~ 1

Author(s):

Xi Chen

Keyword(s):

Formal Verification ◽

Control Algorithm ◽

Theorem Prover ◽

Automatic Landing ◽

Landing Control

Download Full-text

Evaluation Opportunities in Mechanized Theories

10.29007/7kx8 ◽

2018 ◽

Author(s):

Joe Hurd

Keyword(s):

Mathematical Theory ◽

Theorem Prover ◽

Mechanized Mathematics ◽

Reasoning Tasks

This invited talk will look at logic solvers through the application lens of constructing and processing a theory library of mechanized mathematics. In fact, constructing and processing theories are two distinct applications, and each will be considered in turn. Construction is carried out by formalizing a mathematical theory using an interactive theorem prover, and logic solvers can remove much of the drudgery by automating common reasoning tasks. At the theory library level, logic solvers can provide assistance with theory engineering tasks such as compressing theories, managing dependencies, and constructing new theories from reusable theory components.

Download Full-text

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

Journal of Functional Programming ◽

10.1017/s0956796821000022 ◽

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).

Download Full-text

Cosmo: a concurrent separation logic for multicore OCaml

Proceedings of the ACM on Programming Languages ◽

10.1145/3408978 ◽

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

Download Full-text