ABSTRACT. Monadic decomposability is a notion of variable independence, which asks whether a given formula in a first-order theory is expressible as a boolean combination of monadic predicates in the theory. Recently, Veanes et al. showed the usefulness of monadic decomposability in the context of SMT (i.e. input formula is quantifier-free), and found various interesting applications including string analysis. Despite these, checking monadic decomposability is undecidable in general. Decidability for certain theories is known (e.g. Presburger Arithmetic, Tarski's Real Closed Field), but there are very few results regarding their computational complexity. In this paper, we study monadic decomposability of integer linear arithmetic in the setting of SMT. We show that this decision problem is coNP-complete and, when monadically decomposable, a formula admits a decomposition of exponential size in the worst case. We provide a new application of our results to string constraint solving with length constraints. We then extend our results to variadic decomposability, where predicates could admit multiple free variables (in contrast to monadic decomposability). We provide an application to quantifier elimination in integer linear arithmetic where the variables in a block of quantifiers, if independent, could be eliminated with an exponential (instead of the standard double exponential) blow-up.

ABSTRACT. Fixed-point arithmetic is a popular alternative to floating-point arithmetic on embedded systems. Existing work on the verification of fixed-point programs relies on custom formalizations of fixed-point arithmetic, which makes it hard to compare the described techniques or reuse the implementations. In this paper, we address this issue by proposing and formalizing an SMT theory of fixed-point arithmetic. We present an intuitive yet comprehensive syntax of the fixed-point theory, and provide formal semantics for it based on rational arithmetic. We also describe two decision procedures for this theory: one based on the theory of bit-vectors and the other on the theory of reals. We implement the two decision procedures, and evaluate our implementations using existing mature SMT solvers on a benchmark suite we created. Finally, we perform a case study of using the theory we propose to verify properties of quantized neural networks.

ABSTRACT. The abduction problem asks whether there exists a predicate that is consistent with a given set of axioms that when added to these axioms suffices to entail a goal. We propose an approach for solving the abduction problem that is based on syntax-guided enumeration in the Satisfiability Modulo Theories (SMT) solver CVC4. For scalability, we use a novel algorithm that incrementally constructs a solution in disjunctive normal form that is built from enumerated predicates. The algorithm can be configured to generate progressively weaker and simpler solutions over the course of a run of the algorithm. Our approach is fully general and can be applied over any background logic that is handled by the underlying SMT solver in our approach. Our experiments show our approach compares favorably with other tools for abductive reasoning.

ABSTRACT. We address the problem of proving the satisfiability of Constrained Horn Clauses (CHCs) with Algebraic Data Types (ADTs), such as lists and trees. We propose a technique that transforms sets of CHCs with ADTs into CHCs where predicates are defined over basic types, such as integers and booleans, only. We show that if the set of transformed clauses is satisfiable, then so is the set of the original clauses. Thus, our technique avoids the explicit use of inductive proof rules during satisfiability proofs. The main extension over previous techniques is that the transformation automatically generates new predicates corresponding to the lemmata that are often needed by inductive proofs. By an experimental evaluation, we show that our approach is competitive with respect to techniques that extend CHC solving with induction.

ABSTRACT. Sorting algorithms are an important part of most standard libraries, and both, their correctness and efficiency is crucial for many applications.

As generic sorting algorithm, the GNU C++ Standard Library implements the Introsort algorithm, a combination of quicksort, heapsort, and insertion sort. The Boost C++ library implements Pdqsort, an extension of Introsort that achieves linear runtime on inputs with certain patterns.

We verify Introsort and Pdqsort in the Isabelle LLVM verification framework, including most of the optimizations from the GNU and Boost implementations. On an extensive benchmark set, our verified algorithms perform on par with the originals.

ABSTRACT. Liveness analysis is a standard compiler analysis, enabling several optimizations such as deadcode elimination. The SSA form is a popular compiler intermediate language allowing for simple and fast optimizations. Boissinot et al. designed a fast liveness analysis by combining the specific properties of SSA with graph-theoretic ideas such as depth-first search and dominance. We formalize their approach in the Coq proof assistant, inside the CompCertSSA verified C compiler. We also compare experimentally this approach on CompCert's benchmarks with respect to the classic dataflow-based liveness analysis, and observe performance gains.

ABSTRACT. We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, load balancing, and bin packing. In the process we uncover incompletenesses in existing proofs and improve the approximation ratio in one case.

ABSTRACT. We verify two related divide-and-conquer algorithms solving one of the fundamental problems in Computational Geometry, the Closest Pair of Points problem. Using the interactive theorem prover Isabelle/HOL, we prove functional correctness and the optimal running time of O(n log n) of the algorithms. We generate executable code which is empirically competitive with handwritten reference implementations.

ABSTRACT. We have modified the Vampire theorem prover to support rank-1 polymorphism. In this paper we discuss the changes required to enable this and compare the performance of polymorphic Vampire against other polymorphic provers. We also compare its performance on monomorphic problems against standard Vampire. Finally, we discuss how polymorphism can be used to support theory reasoning and present results related to this.

ABSTRACT. iProver is a saturation theorem prover for first-order logic with equality, which is originally based on an instantiation calculus, Inst-Gen. In this paper we describe an extension of iProver with the superposition calculus. We have developed a flexible simplification setup that subsumes and generalises common architectures such as Discount or Otter. This also includes the concept of "immediate simplification", wherein newly derived clauses are more aggressively simplified among themselves, which can make the given clause redundant and thus its children discarded, and the concept of "light normalisation", wherein ground unit equations are stored in an interreduced TRS which is then used to simplify new clauses. We have also added support for associative-commutative theories (AC), namely by deletion of AC-joinable clauses, semantic detection of AC axioms, and preprocessing normalisation.

ABSTRACT. PyRes is a complete theorem prover for first-order logic. It is not designed for high performance, but to clearly demonstrate the core concepts of a saturating theorem prover. The system is written in extensively commented Python, explaining data structures, algorithms, and many of the underlying theoretical concepts. The prover implements binary resolution with factoring and optional negative literal selection. Equality is handled by adding the basic axioms of equality. PyRes uses the given-clause algorithm, optionally controlled by weight- and age evaluations for clause selection. The prover can read TPTP CNF/FOF input files and produces TPTP/TSTP proof objects.

Evaluation shows, as expected, mediocre performance compared to modern high-performance systems, with relatively better performance for problems without equality. However, the system seems to be sound and complete in practice.

ABSTRACT. We describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision procedures such as SMT, semi-automatic inductive provers of the Boyer-Moore family like ACL2, and interactive proof assistants for typed higher-order logics. Imandra's logic is computational, based on a pure subset of OCaml in which all functions are terminating, with restrictions on types and higher-order functions that allow conjectures to be translated into multi-sorted first-order logic with theories, including arithmetic and datatypes. Imandra has novel features supporting large-scale industrial applications, including a seamless integration of bounded and unbounded verification, first-class computable counterexamples, efficiently executable models and a cloud-native architecture supporting live multiuser collaboration. % The core reasoning mechanisms of Imandra are \begin{inparaenum}[(i)] \item a semi-complete procedure for finding models of formulas in the logic mentioned above, centered around the lazy expansion of recursive functions, \item an inductive waterfall and simplifier which ``lifts'' many Boyer-Moore ideas to our typed higher-order setting. \end{inparaenum} % These mechanisms are tightly integrated and subject to many forms of user control. Imandra's user interfaces include an interactive toplevel, Jupyter notebooks and asynchronous document-based verification (in the spirit of Isabelle's Prover IDE) with VS Code.

ABSTRACT. Modern logic engines widely fail to decide axiom sets that are only satisfiable in an infinite domain. This paper specifies a method to decide an infinite number of infinity axiom sets by strong infinity axiom sets (superpostulates). Any formula that is derivable from satisfiable superpostulates is also satisfiable. Starting from known infinity axioms, a complete infinity axiom set for pure first-order logic with only one binary relation (FOL$_{R}$) is specified. Based on complete theories, rules are defined to generate a system of infinity superpostulates based on a complete infinity axiom set. We generated a database with 1040 infinity superpostulates by running our algorithm. The paper ends with a discussion of the possibility of extending the method of specifying infinity superpostulates for FOL$_{R}$.

ABSTRACT. Coinductive reasoning about infinitary data structures has many applications in computer science. Nonetheless developing natural proof systems (especially ones amenable to automation) for reasoning about coinductive data remains a challenge. This paper presents a minimal, generic formal framework that uniformly captures applicable (i.e. finitary) forms of inductive and coinductive reasoning in an intuitive manner. The logic extends transitive closure logic, a general purpose logic for inductive reasoning based on the transitive closure operator, with a dual 'co-closure' operator that similarly captures applicable coinductive reasoning in a natural, effective manner. We develop a sound and complete non-well-founded proof system for the extended logic, whose cyclic subsystem provides the basis for an effective system for automated inductive and coinductive reasoning. To demonstrate the adequacy of the framework we show that it captures the canonical coinductive datatype: streams.