Formal Reasoning about Decentralized Financial Applications

ABSTRACT. Financial applications such as Landing and Payment protocols, and their realization in decentralized financial (DeFi) applications in Blockchains, comprise a unique domain where bugs in the code may be exploited by anyone to steal assets. This situation provides unique opportunities for formal verification to enable “move fast and break nothing”. Formal verification can be used to detect errors early in the development process and guarantee correctness when a new version of the code is deployed.I will describe an attempt to automatically verify DeFis and identify potential bugs. The approach is based on breaking the verification of DeFis into decidable verification tasks. Each of these tasks is solved via a decision procedure which automatically generates a formal proof or a test input showing a violation of the specification. In order to overcome undecidability, high level properties are expressed as ghost states and static analysis used to infer how low level programs update ghost states.

The ksmt calculus is a delta-complete decision procedure for non-linear constraints

ABSTRACT. ksmt is a CDCL-style calculus for solving non-linear constraints over real numbers involving polynomials and transcendental functions. In this paper we investigate properties of the ksmt calculus and show that it is a delta-complete decision procedure. We also propose an extension with local linearisations, which allow for efficient treatment of non-linear constraints.

Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning

ABSTRACT. The problem of invariant checking in parametric systems -- which are
required to operate correctly regardless of the number and connections of
their components -- is gaining increasing importance in various sectors,
such as communication protocols and control software.
Such systems are typically modeled using quantified formulae, describing
the behaviour of an unbounded number of (identical) components,
and their automatic verification often relies on the use of decidable
fragments of first-order logic in order to effectively deal with the
challenges of quantified reasoning.

In this paper, we propose a fully automatic technique for invariant
checking of parametric systems which does not rely on quantified
reasoning. Parametric systems are modeled with array-based transition
systems, and our method iteratively constructs a quantifier-free
abstraction by analyzing, with SMT-based invariant checking algorithms for
non-parametric systems, increasingly-larger finite instances of the
parametric system. Depending on the verification result in the concrete
instance, the abstraction is automatically refined by leveraging canditate
lemmas from inductive invariants, or by discarding previously computed
lemmas.

We implemented the method using a quantifier-free SMT-based IC3 as
underlying verification engine. Our experimental evaluation
demonstrates that the approach is competitive with the state of the art,
solving several benchmarks that are out of reach for other tools.

Tableau-based decision procedure for non-Fregean logic of sentential identity

ABSTRACT. Sentential Calculus with Identity (SCI) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of SCI-formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for SCI which runs in NP, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: decomposition and equality rules, whose interplay yields derivation trees with branches of polynomial length with respect to the size of the investigated formula. We describe an implementation of the procedure and compare its performance with implementations of other calculi for SCI} (for which, however, the termination results were not established). We show possible refinements of our algorithm and discuss the possibility of extending it to other non-Fregean logics.

Learning from Łukasiewicz and Meredith: Investigations into Proof Structures

ABSTRACT. The material presented in this paper contributes to
establishing a basis deemed essential for substantial
progress in Automated Deduction. It identifies and studies
global features in selected problems and their proofs which
offer the potential of guiding proof search in a more direct
way. The studied problems are of the wide-spread form of
"axiom(s) and rule(s) imply goal(s)". The features include
various proof structures and the well-known concept of
lemmas. For their elaboration both human and automated
proofs of selected theorems are taken into a close
comparative consideration. The study at the same time
accounts for a coherent and comprehensive formal
reconstruction of historical work by Łukasiewicz, Meredith
and others. First experiments resulting from the study
indicate novel ways of lemma generation to supplement
automated first-order provers of various families,
strengthening in particular their ability to find short
proofs.

ABSTRACT. We present novel reductions of the propositional modal logics KB, KD, KT, K4 and K5 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 \KSP to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover KSP performs well when compared with a specialised resolution calculus for these logics and with the in-built reductions of the first-order prover SPASS.

Isabelle's Metalogic: Formalization and Proof Checker

ABSTRACT. Isabelle is a generic theorem prover with a fragment of higher-order
logic as a metalogic for defining object logics. Isabelle also
provides proof terms. We formalize this metalogic and the language of
proof terms in Isabelle/HOL, define an executable (but inefficient)
proof term checker and prove its correctness w.r.t. the metalogic.
We integrate the proof checker with Isabelle and run it on a range of logics
and theories to check the correctness of all the proofs in those theories.

Unifying Decidable Entailments in Separation Logic with Inductive Definitions

ABSTRACT. The entailment problem in Separation Logic, between separated conjunctions of
equational, spatial and predicate atoms, interpreted by a finite set of inductive rules, is undecidable in general. Certain restrictions on the set of inductive definitions lead to decidable classes of entailment problems. Currently, there are two such decidable classes, based on two restrictions, called establishment and restrictedness, respectively. Both classes are shown to be in 2EXPTIME by two independent proofs and a many-one reduction of established to restricted entailment problems has been given. In this paper, we strictly generalize the restricted class, by distinguishing the conditions that apply only to the left and the right hand side of entailments, respectively. We provide a many-one reduction of this generalized class, called safe, to the established class. Together with the reduction of established to restricted entailment problems, this new reduction closes the loop and shows that the three classes of entailment problems (respectively established, restricted and safe) form a single, unified, 2EXPTIME-complete class.

Subformula Linking for Intuitionistic Logic and Type Theory

ABSTRACT. Subformula linking is an interactive theorem proving technique that was initially proposed for (classical) linear logic. It is based on truth and context preserving rewrites of a conjecture that are triggered by a user indicating directed edges between subformulas, which can be done without tactics or proof languages. The system guarantees that a true conjecture can always be rewritten to a known, usually trivial, theorem. In this work we extend this technique to intuitionistic logic and type theory in three steps. First, we extend subformula linking to intuitionistic first-order logic. Next, we show how to integrate simply typed lambda-terms as the term language of this logic. Finally we rely on a simple embedding of intuitionistic type theory into this logic, and discuss hiding the embedding from the end user's perspective.

Efficient SAT-based proof search in Intuitionistic Propositional Logic

ABSTRACT. We present an efficient proof search procedure for Intuitionistic Propositional Logic which involves the use of an incremental SAT-solver. Basically, it is obtained by adding a restart operation to the system intuit by Claessen and Rosén,thus we call our implementation intuitR. We gain some remarkable advantages: derivations have a simple structure; countermodels are in general small; using a standard benchmarks suite, we outperform intuit and other state-of-the-art provers.

Proof Search and Certificates for Evidential Transactions

ABSTRACT. Attestation logics have been used for specifying systems with policies
involving different principals. Cyberlogic is an attestation logic used
for the specification of Evidential Transactions (ETs).
In such transactions, evidence has to be provided supporting its
validity with respect to given policies. For example, visa applicants
must demonstrate that they have sufficient funds to visit a foreign
country. Such evidence can be expressed as a Cyberlogic proof,
possibly combined with non-logical data (e.g., a digitally signed
document). A key issue is how to construct and communicate such
evidence/proofs. It turns out that attestation modalities makes it
challenging to use established proof-theoretic methods such as focusing.
Our first contribution is the refinement of Cyberlogic proof theory
with knowledge operators which can be used to represent knowledge
bases local to one or more principals. Our second contribution is
the identification of a fragment of Cyberlogic, called Cyberlogic
programs, enabling the specification of ETs.
Our third contribution is a sound and complete proof system for
Cyberlogic programs enabling proof search similar to search in logic
programming. Our final contribution is a proof certificate format
for Cyberlogic programs inspired by Foundational Proof Certificates
as a means to communicate evidence and check its validity.

The CADE-28 (online) reception, a time to meet and interact with friends and foes in the automated reasoning community. It's open bar (BYO), tasty hors d'oeuvres(BYO), and live entertainment ... there will be five "topical sessions", each led by experts in the topical areas. To start it off the experts will give 5 minute teasers for their topics. Then for the second 30 minutes there will be five breakout ZoomRooms in which the experts will lead and listen to discussion of their topics. People can join and leave the topical rooms, to enjoy some interesting interactions. Remember that the ChatRooms are available if you want head off for a private discussion.