For over two decades Separation Logic has enjoyed its unique position as arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and permissions. Separation Logic is often extended to include inductively-defined predicates, interpreted as least fixpoints, to form what is known as Separation Logic with Inductive Definitions (SLID). These inductive predicates are used to describe unbounded data-structures in the heap and to verify key properties thereof. Many theoretical and practical advances have been made in developing automated proof mechanisms for SLID, but by their very nature these mechanisms are imperfect, and a deeper understanding of their failures is desired. As expressive as Separation Logic is, it is not surprising that it is incomplete: there is no procedure that will provide a proof for all valid entailments in Separation Logic. In fact, at its very core, Separation Logic contains several sources of incompleteness that defy automated reasoning. In this paper we study these sources of incompleteness and how they relate to failures of proof mechanisms of SLID. We contextualize SLID within a larger, relaxed logic, that we call Weak Separation Logic (WSL). We prove that unlike SLID, WSL enjoys completeness for a non-trivial fragment of quantified entailments with background theories and inductive definitions, via a reduction to first-order logic (FOL). Moreover, we show that the ubiquitous fold/unfold proof mechanism, which is unsurprisingly incomplete for SLID, does constitute a sound and complete proof mechanism of WSL, for theory-free, quantifier-free entailments with inductive definitions. In some sense, this shows that WSL is the natural logic of such proof mechanisms. Through this contextualization of SLID within WSL, we understand proof failures as stemming from rogue, nonstandard models, that exist within the class of models considered by WSL, but do not adhere to the stricter requirements of SLID. These rogue models are typically infinite, and we use the recently proposed formalism of symbolic structures to represent and automatically find them. We present a prototype tool that implements the encoding of WSL to FOL and test it on an existing benchmark, which contains over 700 quantified entailment problems with inductive definitions, a third of which also contain background theories. Our tool is able to find counter-models to many of the examples, and we provide a partial taxonomy of the rogue models, shedding some light on real-world proof failures.

We consider the problem of verification modulo tested library contracts as a step towards automating the verification of client programs that use complex libraries. We formulate this problem as the synthesis of modular contracts for the library methods used by the client that are adequate to prove the client correct, and that also pass the scrutiny of a testing engine that tests the library against these contracts. We also consider a new form of method contracts called contextual contracts that arise in this setting that hold in the context of the client program, and can often be simpler and easier to infer than classical modular contracts. We provide a counterexample-guided learning framework to solve this problem, in which the synthesizer interacts with a constraint solver as well as the testing engine in order to infer adequate modular/contextual method contracts and inductive invariants for the client. The main synthesis engines we use are generalizing CHC solvers that are realized using ICE learning algorithms. We realize this framework in a tool called Dualis and show its efficacy on benchmarks where clients call large libraries.

Program verification techniques for expressive heap logics are inevitably incomplete. In this work we argue that algorithmic techniques for reasoning with expressive heap logics can be held up to a different robust theoretical standard for completeness: FO-Completeness. FO-completeness is a theoretical guarantee that all theorems that are valid when recursive definitions are interpreted as fixpoint definitions (instead of least fixpoint) are guaranteed to be eventually proven by the system. We illustrate a set of principles to design such logics and develop the first two heap logics that have implicit heaplets and that admit FO-Complete program verification. The logics we develop are a frame logic (FL) and a separation logic (SL-FL) that has an alternate semantics inspired by frame logic. We show a verification condition generation technique that is amenable to FO-complete reasoning using quantifier instantiation and SMT solvers. We implement tools that realize our technique and show the expressiveness of our logics and the efficacy of the verification technique on a suite of benchmarks that manipulate data structures.

We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using B oogie and prove a suite of data structure manipulating programs correct.

Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact complete for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explain why they fail when they fail, and the precise role that user help plays in making proofs succeed.

We propose a novel logic, Frame Logic (FL), that extends first-order logic and recursive definitions with a construct Sp (·) that captures the implicit supports of formulas—the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in frame logic.

We consider the problem of combining machine learning models to perform higher-level cognitive tasks with clear specifications. We propose the novel problem of Visual Discrimination Puzzles (VDP) that requires finding interpretable discriminators that classify images according to a logical specification. Humans can solve these puzzles with ease and they give robust, verifiable, and interpretable discriminators as answers. We propose a compositional neurosymbolic framework that combines a neural network to detect objects and relationships with a symbolic learner that finds interpretable discriminators. We create large classes of VDP datasets involving natural and artificial images and show that our neurosymbolic framework performs favorably compared to several purely neural approaches.

Axioms and inference rules form the foundation of deductive systems and are crucial in the study of reasoning with logics over structures. Historically, axiomatizations have been discovered manually with much expertise and effort. In this paper we show the feasibility of using synthesis techniques to discover axiomatizations for different classes of structures, and in some contexts, automatically prove their completeness. For evaluation, we apply our technique to find axioms for (1) classes of frames in modal logic characterized in first-order logic and (2) the class of language models with regular operations.

Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (FO+lfp) with background theories. Such logics, unlike pure first-order logic, do not admit even complete procedures. In this paper, we undertake a novel approach for synthesizing inductive hypotheses to prove validity in this logic. The idea is to utilize several kinds of finite first-order models as counterexamples that capture the non-provability and invalidity of formulas to guide the search for inductive hypotheses. We implement our procedures and evaluate them extensively over theorems involving heap data structures that require inductive proofs and demonstrate the effectiveness of our methodology.

We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class use uninterpreted functions and relations, and abide by a restriction called coherence that was recently identified to yield decidable verification. We formulate a powerful grammar-restricted (syntax-guided) synthesis problem for coherent uninterpreted programs, and we show the problem to be decidable, identify its precise complexity, and also study several variants of the problem.

Abstract We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct $$\textit{Sp}(\cdot )$$ Sp ( · ) that captures the implicit supports of formulas— the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL.

We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We extend recent work that identified a decidable subclass of uninterpreted programs to a class of alias-aware programs that can update maps. We apply this theory to develop verification algorithms for memory safety— determining if a heap-manipulating program that allocates and frees memory locations and manipulates heap pointers does not dereference an unallocated memory location. We show that this problem is decidable when the initial allocated heap forms a forest data-structure and when programs are streaming-coherent , which intuitively restricts programs to make a single pass over a data-structure. Our experimental evaluation on a set of library routines that manipulate forest data-structures shows that common single-pass algorithms on data-structures often fall in the decidable class, and that our decision procedure is efficient in verifying them.

We report on the development of a blockchain system that is significantly verified and performant, detailing the design, proof, and system development based on a process of continuous refinement. We instantiate this framework to build, to the best of our knowledge, the first blockchain (Kaizen) that is performant and verified to a large degree, and a cryptocurrency protocol (KznCoin) over it. We experimentally compare its performance against the stock Bitcoin implementation.