Abstract We present —a Dafny-style verifier for imperative programs embedded in the Lean proof assistant. Like Dafny, supports reasoning about effectful programs featuring mutable state, loops, and non-determinism. Unlike Dafny, seamlessly combines automated SMT-based proofs with the interactive proof mode of the Lean proof assistant, in which it is embedded, thus enabling multi-modal proofs. Implemented as a Lean library, enjoys interaction with the rest of the Lean ecosystem, and in particular, with its automation tactics and rich library of mathematical theories. In this paper, we give a tour of ’s features, outline the techniques underlying its implementation, and evaluate its performance and expressivity in comparison with Dafny.

Multi-modal program verification is a process of validating code against its specification using both dynamic and symbolic techniques, and proving its correctness by a combination of automated and interactive machine-assisted tools. In order to be trustworthy, such verification tools must themselves come with formal soundness proofs, establishing that any program verified in them against a certain specification does not violate the specification’s statement when executed. Verification tools that are proven sound in a general-purpose proof assistant with a small trusted core are commonly referred to as foundational . We present a framework that facilitates and streamlines construction of program verifiers that are both foundational and multi-modal. Our approach adopts the well-known idea of monadic shallow embedding of an executable program semantics into the programming language of a theorem prover based on higher-order logic, in our case, the Lean proof assistant. We provide a library of monad transformers for such semantics, encoding a variety of computational effects, including state, divergence, exceptions, and non-determinism. The key theoretical innovation of our work are monad transformer algebras that enable automated derivation of the respective sound verification condition generators. We show that proofs of the resulting verification conditions enjoy automation using off-the-shelf SMT solvers and allow for an interactive proof mode when automation fails. To demonstrate versatility of our framework, we instantiated it to embed two foundational multi-modal verifiers into Lean for reasoning about (1) distributed protocol safety and (2) Dafny-style specifications of imperative programs, and used them to mechanically verify a number of non-trivial case studies.

Abstract We present , an open-source framework for automated and interactive verification of transition systems, aimed specifically at conducting machine-assisted proofs about concurrent and distributed algorithms. is implemented on top of the proof assistant. It allows one to describe a transition system and its specification in a simple imperative language, producing verification conditions in first-order logic, to be discharged automatically via a range of SMT solvers. In case automated verification fails or if the system’s description requires statements in a higher-order logic, provides an interactive verification mode, by virtue of being embedded in a general-purpose proof assistant. We have evaluated on a large set of case studies from the distributed system verification literature, showing that its automated verification performance is acceptable for practical verification tasks, while it also allows for seamless automated/interactive verification of system specifications beyond the reach of existing automated provers.

To meet the increasing demand for customized software, highly configurable systems become essential in practice. Such systems offer many options to configure, and ensuring the reliability of these systems is critical. A widely used evaluation metric for testing these systems is \(t\) -wise coverage, where \(t\) represents testing strength, and its value typically ranges from 2 to 6. It is crucial to design effective and efficient methods for generating test suites that achieve high \(t\) -wise coverage. However, current state-of-the-art methods need to generate large test suites for achieving high \(t\) -wise coverage. In this work, we propose a novel method called LS-Sampling-Plus that can efficiently generate test suites with high \(t\) -wise coverage for \(2\leq t\leq 6\) while being smaller in size compared to existing state-of-the-art methods. LS-Sampling-Plus incorporates many core algorithmic techniques, including two novel scoring functions, a dynamic mechanism for updating sampling probabilities, and a validity-guaranteed systematic search method. Our experiments on various practical benchmarks show that LS-Sampling-Plus can achieve higher \(t\) -wise coverage than current state-of-the-art methods, through building a test suite of the same size. Moreover, our evaluations indicate the effectiveness of all core algorithmic techniques of LS-Sampling-Plus . Furthermore, LS-Sampling-Plus exhibits better scalability and fault detection capability than existing state-of-the-art methods.

Byzantine Fault-Tolerant (BFT) protocols are known to be difficult to design and to reason about. To address this challenge, on one hand, several approaches have been developed recently for computer-aided formal verification of the desired correctness properties, both safety and liveness, of standalone BFT protocols. On the other hand, the distributed computing community has made attempts to reduce the conceptual complexity of constructing new such protocols by showing how to assemble them from simpler "building blocks". No methodology to date combines these two approaches for foundational verification of arbitrary BFT protocols.

Array-based encodings of tree structures are often preferable to linked or abstract data type-based representations for efficiency reasons. Compared to the more traditional encodings, array-based trees do not immediately offer convenient induction principles, and the programs that manipulate them often implement traversals non-recursively, requiring complex loop invariants for their correctness proofs.

To meet the rising demand for software customization, highly configurable software systems play key roles in practice. Combinatorial interaction testing (CIT) is recognized as an effective approach for testing such systems. For CIT, the most important problem is constrained covering array generation (CCAG), which aims to construct a minimum-sized t-wise covering array (CA), where t denotes testing strength. Compared to pairwise testing (i.e., 2-wise CIT) that is a widely-used CIT technique, 3-wise CIT can discover more faults and bring more benefit in real-world applications. However, current state-of-the-art CCAG algorithms suffer from the severe scalability challenge for 3-wise CIT, which renders them ineffective in building 3-wise CAs for highly configurable systems. In this work, we perform an empirical study on various practical, highly configurable systems to present that it is promising to build 3-wise CA through extending 2-wise CA. Inspired by this, we propose ScalableCA, a novel and scalable algorithm that can effectively alleviate the scalability challenge for 3-wise CIT. Further, ScalableCA introduces three new and effective techniques, including fast invalidity detection, uncovering-guided sampling, and remainder-aware local search, to enhance its performance. Our experiments on extensive real-world, highly configurable systems show that, compared to current state-of-the-art algorithms, ScalableCA requires one to two orders of magnitude less running time to build 3-wise CA of 38.9% smaller size in average for large-scale instances. Our results indicate that ScalableCA greatly advances the state of the art in 3-wise CIT.

Arrays are a fundamental abstraction to represent collections of data. It is often possible to exploit structural properties of the data stored in an array ( e.g ., repetition or sparsity) to develop a specialised representation optimised for space efficiency. Formally reasoning about correctness of manipulations with such structured data is challenging, as they are often composed of multiple loops with non-trivial invariants. In this work, we observe that specifications for structured data manipulations can be phrased as hypersafety properties, i.e ., predicates that relate traces of k programs. To turn this observation into an effective verification methodology, we developed the Logic for Graceful Tensor Manipulation (LGTM), a new Hoare-style relational separation logic for specifying and verifying computations over structured data. The key enabling idea of LGTM is that of parametrised hypersafety specifications that allow the number k of the program components to depend on the program variables . We implemented LGTM as a foundational embedding into Coq, mechanising its rules, meta-theory, and the proof of soundness. Furthermore, we developed a library of domain-specific tactics that automate computer-aided hypersafety reasoning, resulting in pleasantly short proof scripts that enjoy a high degree of reuse. We argue for the effectiveness of relational reasoning about structured data in LGTM by specifying and mechanically proving correctness of 13 case studies including computations on compressed arrays and efficient operations over multiple kinds of sparse tensors.

The increasing demand for software customization has led to the development of highly configurable systems. Combinatorial interaction testing (CIT) is an effective method for testing these types of systems. The ultimate goal of CIT is to generate a test suite of acceptable size, called a t-wise covering array (CA), where t is the testing strength. Pairwise testing (i.e., CIT with t=2) is recognized to be the most widely-used CIT technique and has strong fault detection capability. In pairwise testing, the most important problem is pairwise CA generation (PCAG), which is to generate a pairwise CA (PCA) of minimum size. However, existing state-of-the-art PCAG algorithms suffer from the severe scalability challenge; that is, they cannot tackle large-scale PCAG instances effectively, resulting in PCAs of large sizes. To alleviate this challenge, in this paper we propose CAmpactor, a novel and effective local search algorithm for compacting given PCAs into smaller sizes. Extensive experiments on a large number of real-world, public PCAG instances show that the sizes of CAmpactor's generated PCAs are around 45% smaller than the sizes of PCAs constructed by existing state-of-the-art PCAG algorithms, indicating its superiority. Also, our evaluation confirms the generality of CAmpactor, since CAmpactor can reduce the sizes of PCAs generated by a variety of PCAG algorithms.

Combinatorial interaction testing (CIT) is an effective paradigm for testing highly configurable systems, and its goal is to generate a t-wise covering array (CA) as a test suite, where t is the strength of testing. It is recognized that pairwise testing (i.e., CIT with t=2) is the most common CIT technique, and has high fault detection capability in practice. The problem of pairwise CA generation (PCAG), which is a core problem in pairwise testing, aims at generating a pairwise CA (i.e., 2-wise CA) of minimum size, subject to hard constraints. The PCAG problem is a hard combinatorial optimization problem, which urgently requires practical methods for generating pairwise CAs (PCAs) of small sizes. However, existing PCAG algorithms suffer from the severe scalability issue; that is, when solving large-scale PCAG instances, existing state-of-the-art PCAG algorithms usually cost a fairly long time to generate large PCAs, which would make the testing of highly configurable systems both ineffective and inefficient. In this paper, we propose a novel and effective sampling-based approach dubbed SamplingCA for solving the PCAG problem. SamplingCA first utilizes sampling techniques to obtain a small test suite that covers valid pairwise tuples as many as possible, and then adds a few more test cases into the test suite to ensure that all valid pairwise tuples are covered. Extensive experiments on 125 public PCAG instances show that our approach can generate much smaller PCAs than its state-of-the-art competitors, indicating the effectiveness of SamplingCA. Also, our experiments show that SamplingCA runs one to two orders of magnitude faster than its competitors, demonstrating the efficiency of SamplingCA. Our results confirm that SamplingCA is able to address the scalability issue and considerably pushes forward the state of the art in PCAG solving.