Solving constrained Horn clauses modulo algebraic data types and recursive functions

This work addresses the problem of verifying imperative programs that manipulate data structures, e.g., Rust programs. Data structures are usually modeled by Algebraic Data Types (ADTs) in verification conditions. Inductive invariants of such programs often require recursively defined functions (RDFs) to represent abstractions of data structures. From the logic perspective, this reduces to solving Constrained Horn Clauses (CHCs) modulo both ADT and RDF. The underlying logic with RDFs is undecidable. Thus, even verifying a candidate inductive invariant is undecidable. Similarly, IC3-based algorithms for solving CHCs lose their progress guarantee: they may not find counterexamples when the program is unsafe. We propose a novel IC3-inspired algorithm Racer for solving CHCs modulo ADT and RDF (i.e., automatically synthesizing inductive invariants, as opposed to only verifying them as is done in deductive verification). Racer ensures progress despite the undecidability of the underlying theory, and is guaranteed to terminate with a counterexample for unsafe programs. It works with a general class of RDFs over ADTs called catamorphisms. The key idea is to represent catamorphisms as both CHCs, via relationification , and RDFs, using novel abstractions . Encoding catamorphisms as CHCs allows learning inductive properties of catamorphisms, as well as preserving unsatisfiabilty of the original CHCs despite the use of RDF abstractions, whereas encoding catamorphisms as RDFs allows unfolding the recursive definition, and relying on it in solutions. Abstractions ensure that the underlying theory remains decidable. We implement our approach in Z3 and show that it works well in practice.

Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.

The Quietist Posit: A Methodologically Agnostic Resolution to the Problem of Qualia

<p>This thesis paper addresses the aim and methodology of an argument by Daniel Dennett (1988; 1992), who proposes an eliminativism with regards to the referent of the term “qualia”. Dennett’s argument centres on the purported failure for any property to meet the criteria for this term widely found in traditional philosophical literature. Dennett argues that this failure may be demonstrated as a result of the term failing to refer to any property which contains naturalistic methodological verification conditions. I provide, in this paper, an outline of two key historical arguments by W.V. Quine and Ludwig Wittgenstein, respectively, whose influence on Dennett’s position will help clarify a certain vulnerability in the latter’s argument. I then provide a series of arguments to serve as important counterexamples to the methodology employed by Dennett which, I argue, reveal a dialectical stalemate between two sets of competing methodologies –methodological naturalism and phenomenology. I argue that this stalemate is indicative of a methodological underdetermination with regards to the question of whether qualia exist. I refer to this as the “methodological problem of qualia”. I then propose that a resolution may be found for this problem by adopting a methodological agnosticism. I argue that upon this agnosticism, it is possible to positively assert methodological verification conditions according to which it may be determined whether the term “qualia” refers to a property which contains naturalistic methodological verification conditions. I argue that these are the conditions which hold upon the explicitly conditional, or “methodological”, assumption of a naturalistic methodological verificationism, as opposed to a phenomenological methodology, or vice versa. I conclude that, under these conditions, the term “qualia” therefore may succeed in referring to a property which contains naturalistic methodological verification conditions. As such, I propose that Dennett is incorrect: neither the term nor its referent merit elimination, but rather the latter a quietist resolution, and the former its own meaningful place in language.</p>

The Quietist Posit: A Methodologically Agnostic Resolution to the Problem of Qualia

<p>This thesis paper addresses the aim and methodology of an argument by Daniel Dennett (1988; 1992), who proposes an eliminativism with regards to the referent of the term “qualia”. Dennett’s argument centres on the purported failure for any property to meet the criteria for this term widely found in traditional philosophical literature. Dennett argues that this failure may be demonstrated as a result of the term failing to refer to any property which contains naturalistic methodological verification conditions. I provide, in this paper, an outline of two key historical arguments by W.V. Quine and Ludwig Wittgenstein, respectively, whose influence on Dennett’s position will help clarify a certain vulnerability in the latter’s argument. I then provide a series of arguments to serve as important counterexamples to the methodology employed by Dennett which, I argue, reveal a dialectical stalemate between two sets of competing methodologies –methodological naturalism and phenomenology. I argue that this stalemate is indicative of a methodological underdetermination with regards to the question of whether qualia exist. I refer to this as the “methodological problem of qualia”. I then propose that a resolution may be found for this problem by adopting a methodological agnosticism. I argue that upon this agnosticism, it is possible to positively assert methodological verification conditions according to which it may be determined whether the term “qualia” refers to a property which contains naturalistic methodological verification conditions. I argue that these are the conditions which hold upon the explicitly conditional, or “methodological”, assumption of a naturalistic methodological verificationism, as opposed to a phenomenological methodology, or vice versa. I conclude that, under these conditions, the term “qualia” therefore may succeed in referring to a property which contains naturalistic methodological verification conditions. As such, I propose that Dennett is incorrect: neither the term nor its referent merit elimination, but rather the latter a quietist resolution, and the former its own meaningful place in language.</p>

Integrating Cardinality Constraints into Constraint Logic Programming with Sets

Formal reasoning about finite sets and cardinality is important for many applications, including software verification, where very often one needs to reason about the size of a given data structure. The Constraint Logic Programming tool $$\{ log\} $$ provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, although it does not provide cardinality constraints. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into $$\{ log\} $$ . The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the $$\{ log\} $$ tool. In turn, the implementation uses Howe and King’s Prolog SAT solver and Prolog’s CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice. Under consideration in Theory and Practice of Logic Programming (TPLP)

Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types

A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them.This tool paper describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.

Automatic Generation and Validation of Instruction Encoders and Decoders

Verification of instruction encoders and decoders is essential for formalizing manipulation of machine code. The existing approaches cannot guarantee the critical consistency property, i.e., that an encoder and its corresponding decoder are mutual inverses of each other. We observe that consistent encoder-decoder pairs can be automatically derived from bijections inherently embedded in instruction formats. Based on this observation, we develop a framework for writing specifications that capture these bijections, for automatically generating encoders and decoders from these specifications, and for formally validating the consistency and soundness of the generated encoders and decoders by synthesizing proofs in Coq and discharging verification conditions using SMT solvers. We apply this framework to a subset of X86-32 instructions to illustrate its effectiveness in these regards. We also demonstrate that the generated encoders and decoders have reasonable performance.