ABSTRACT. The need to solve non-linear arithmetic constraints presents a major obstacle for the automatic verification of smart contracts. In this case study we focus on the two overapproximation techniques used by the industry verification tool Certora Prover: overapproximation of non-linear integer arithmetic using linear integer arithmetic and using non-linear real arithmetic. We compare the performance of contemporary SMT solvers on verification conditions produced by the Certora Prover using these two approximations against the natural non-linear integer arithmetic encoding. Our evaluation shows that use of the overapproximation methods leads to solving a significant number of new problems.

ABSTRACT. Contracts specifying a procedure's behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction.

We propose a logic over symbolic traces able to specify recursive procedures in a modular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics. Our work generalizes contract-based to trace-based deductive verification by extending the notion of state-based contracts to trace-based contracts.

ABSTRACT. The quantification of system reliability is fundamental to the assessment of a system’s safety and resilience, and has been of interest to decision-makers. Since quantifying the system reliability is shown to be computationally intractable, researchers aim to find ap- proximations. Existing approaches to approximate reliability either suffer from poor scal- ability or lack of correctness guarantees. Answer Set Programming (ASP) is a powerful tool for knowledge representation that can specify complex combinatorial problems. In recent years, the new applications of ASP have propelled the emergence of well-engineered ASP systems. This paper proposes a new ASP counting based framework, RelNet-ASP, to approximate or estimate the reliability of a system or network. The framework reduces the problem of reliability estimation to an approximate model counting problem on ASP programs, offering formal guarantees of the estimated reliability. The experimental eval- uation demonstrates that RelNet-ASP outperforms state-of-the-art techniques in terms of both runtime performance and accuracy.

ABSTRACT. This work presents a formalisation in Isabelle/HOL of the extension of Hall’s theorem for finite graphs to countable graphs. The proof uses a formalisation of the authors’ countable set-theoretical version of Hall’s theorem that was proved as a consequence of the marriage-condition characterisation for finite families of sets and a formalisation in Isabelle/HOL of the compactness theorem for propositional logic. The development focuses on maintaining specifications and proofs as closely as possible to textbooks since our primary objective is to increase mathematicians’ interest in using interactive proof assistants. Although this, the specification also includes a concise and more automatised proof using locales and the Isabelle Sledgehammer. The development is a first step toward mechanising infinite versions of results equivalent to Hall’s marriage theorem in contexts other than set theory.

ABSTRACT. Inductive invariant inference is the core problem of program verification, in particular, verification of functional programs over algebraic data types (ADTs). This problem is even more complex for the case of ADTs as it is hard to come up with an abstract domain rich enough to represent properties of practical programs and an effective invariant inference procedure for this domain. Many complementary techniques for different abstract domains for ADTs were developed, yet corresponding tools often diverge on real-life programs because of low expressivity of their abstract domains. Moreover, it was unclear whether they could complement each other. We propose a lightweight approach for combining any existing techniques for different abstract domains collaboratively, i.e., a non-portfolio approach for building a verifier with a more expressive domain from existing verifiers. We instantiate it and obtain an effective inductive invariant inference algorithm in a rich combined domain of elementary and regular ADT invariants essentially for free. Because of the richer domain, collaborations of verifiers converge on strictly larger numbers of safety problems, i.e., the collaboration of verifiers is capable of solving problems that are beyond their abilities on their own. Our implementation of the algorithm is a collaboration of two existing state-of-art inductive invariant inference engines having general-purpose first-order logic solvers as a backend. Finally, we show that our implementation is capable of solving the large amount of CHC-Comp 2022 problems obtained from Haskell verification problems, for which the existing tools diverge.

ABSTRACT. Inference and prediction of routes have become of interest over the past decade owing to a dramatic increase in package delivery and ride-sharing services. Given the underlying combinatorial structure and the incorporation of probabilities, route prediction involves techniques from both formal methods and machine learning. One promising approach for predicting routes is using decision diagrams that are augmented with probability values. However, the effectiveness of this approach depends on the size of the compiled decision diagrams. The scalability of the approach is limited owing to its empirical runtime and space complexity. In this work, our contributions are two-fold: first, we introduce a relaxed encoding that uses a linear number of variables with respect to the number of vertices in a road network graph to significantly reduce the size of resultant decision diagrams. Secondly, instead of a stepwise sampling procedure, we propose a single pass sampling-based route prediction. In our evaluations arising from a real-world road network, we demonstrate that the resulting system achieves around twice the quality of suggested routes while being an order of magnitude faster compared to state-of-the-art.

ABSTRACT. We introduce a language-parametric calculus for k-safety verification - Cartesian Reachability logic (CRL). In recent years, formal verification of hyperproperties has become an important topic in the formal methods community. An interesting class of hyperproperties is known as k-safety properties, which express the absence of a bad k-tuple of execution traces. Many security policies, such as noninterference, and functional properties, such as commutativity, monotonicity, and transitivity, are k-safety properties. A prominent example of a logic which can reason about k-safety properties of software systems is Cartesian Hoare logic (CHL). However, CHL targets a specific, small imperative language. In order to use it for sound verification of programs in a different language, one needs to extend it with the desired features, or to hand-craft a translation. Both these approaches require a lot of tedious, error-prone work.

Unlike CHL, CRL is language-parametric: it can be instantiated with an operational semantics (of a certain kind) of any deterministic language. Its soundness theorem is proved once and for all, with no need to adapt or re-prove it for different languages or their variants. This approach can significantly reduce the development costs of tools and techniques for sound k-safety verification of programs in deterministic languages: for example, of smart contracts written for EVM (the language powering the Ethereum blockchain), which already has an operational semantics serving as a reference.

ABSTRACT. Hyperproperties are commonly used to define information-flow policies and other requirements that reason about the relationship between multiple traces in a system. We consider HyperQPTL -- a temporal logic for hyperproperties that combines explicit quantification over traces with propositional quantification as, e.g., found in quantified propositional temporal logic (QPTL). HyperQPTL therefore truly captures omega-regular relations on multiple traces within a system. As such, HyperQPTL can, e.g., express promptness properties, which state that there exists a common bound on the number of steps up to which an event must have happened. While HyperQPTL has been studied and used in various prior works, thus far, no model-checking tool for it exists. This paper presents AutoHyperQ, a fully-automatic automata-based model checker for HyperQPTL that can cope with arbitrary combinations of trace and propositional quantification. We evaluate AutoHyperQ on a range of benchmarks and, e.g., use it to analyze promptness requirements in a diverse collection of reactive systems. Moreover, we demonstrate that the core of AutoHyperQ can be reused as an effective tool to translate QPTL formulas into omega-automata.