Search

Catamorphisms are functions that are recursively defined on list and trees and, in general, on algebraic data types (ADTs), and are often used to compute suitable abstractions of programs that manipulate ADTs. Examples of catamorphisms include functions that compute size of lists, orderedness of lists, and height of trees. It is well known that program properties specified through catamorphisms can be proved by showing the satisfiability of suitable sets of constrained Horn clauses (CHCs). We address the problem of checking the satisfiability of those sets of CHCs, and we propose a method for transforming sets of CHCs into equisatisfiable sets where catamorphisms are no longer present. As a consequence, clauses with catamorphisms can be handled without extending the satisfiability algorithms used by existing CHC solvers. Through an experimental evaluation on a nontrivial benchmark consisting of many list and tree processing algorithms expressed as sets of CHCs, we show that our technique is indeed effective and significantly enhances the performance of state-of-the-art CHC solvers. [ABSTRACT FROM AUTHOR]

A polynomial program is one in which all assignments are given by polynomial expressions and in which all branching is nondeterministic (as opposed to conditional). Given such a program, an algebraic invariant is one that is defined by polynomial equations over the program variables at each program location.Müller-Olm and Seidl have posed the question of whether one can compute the strongest algebraic invariant of a given polynomial program. In this article, we show that, while strongest algebraic invariants are not computable in general, they can be computed in the special case of affine programs, that is, programs with exclusively linear assignments. For the latter result, our main tool is an algebraic result of independent interest: Given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate. [ABSTRACT FROM AUTHOR]

Abstract interpretation is a well-known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are lost and it is, in principle, guaranteed by construction. Completeness means that the abstract interpreter reports no false alarms for all possible inputs, but this is extremely rare because it needs a very precise analysis.We introduce a weaker notion of completeness, called local completeness, which requires that no false alarms are produced only relatively to some fixed program inputs. Based on this idea, we introduce a program logic, called Local Completeness Logic for an abstract domain A, for proving both the correctness and incorrectness of program specifications. Our proof system, which is parameterized by an abstract domain A, combines over- and underapproximating reasoning. In a provable triple ⊦A [p] c [q], c is a program, q is an under-approximation of the strongest post-condition of c on input p such that their abstractions in A coincide. This means that q is never too coarse, namely, under some mild assumptions, the abstract interpretation of c does not yield false alarms for the input p iff q has no alarm. Therefore, proving ⊦A [p] c [q] not only ensures that all the alarms raised in q are true ones, but also that if q does not raise alarms, then c is correct.We also prove that if A is the straightforward abstraction making all program properties equivalent, then our program logic coincides with O’Hearn’s incorrectness logic, while for any other abstraction, contrary to the case of incorrectness logic, our logic can also establish program correctness. [ABSTRACT FROM AUTHOR]

Many foundational program verification tools have been developed to build machine-checked program correctness proofs, a majority of which are based on Hoare logic. Their program logics, their assertion languages, and their underlying programming languages can be formalized by either a shallow embedding or a deep embedding. Tools like early versions of Verified Software Toolchain (before 2018) choose different shallow embeddings to formalize their program logic. But the pros and cons of these different embeddings were not yet well studied. Therefore, we want to study the impact of the program logic’s embedding on logic’s proof rules in this paper. This paper considers a set of useful extended proof rules, which aided the proof automation in VST, and four different logic embeddings: one deep embedding and three common shallow embeddings. We prove the validity of these extended rules under these embeddings and discuss their main challenges. Furthermore, we propose a method to lift existing shallowly embedded logics to deeply embedded ones to greatly simplify proofs of extended rules in VST. We implemented our theory in VST by lifting the originally shallowly embedded VST to our deeply embedded VST and establishing these extended rules. [ABSTRACT FROM AUTHOR]

Software verification aims to prove that a program satisfies some given properties for all its possible executions. Software evolved incredibly fast during the last century, exposing several challenges to this scientific discipline. The goal of the "Challenges of Software Verification Symposium" is to monitor the state-of-the-art in this field. In this article, we will present the evolution of software from its inception in the 1940s to today's applications, how this exposed new challenges to software verification, and what this discipline achieved. We will then discuss how this chapter covers most of the current open challenges, the possible future software developments, and what challenges this will raise in software verification. [ABSTRACT FROM AUTHOR]

Program deadlock detection plays an important role in ensuring the stability of software systems. In view of the high efficiency and low false alarm rate, dynamic deadlock analysis methods are widely studied. However, existing dynamic analysis methods use lock graph or its extended variants to model program behavior. Since there are information loss in existing lock graphs, deadlock false positives still exist. To solve the problem, a novel 2-stage dynamic deadlock analysis method is proposed. In the first stage, a Petri net model of the program is constructed by analyzing program running traces. Then, unfolding-based Petri net dead marking detection methods are used to identify potential program deadlocks. In the second stage, based on Petri net unfolding techniques, a deterministic program scheduling scheme that can be used for deadlock replay is derived for each potential deadlock. Each successfully replayed program deadlock is a real deadlock. It is shown that the proposed deadlock detection and replay method can eliminate more false positives compared to general dynamic methods, and the deadlock replay scheme is deterministic and easy to understand compared with existing random scheduling strategies.

This paper studies how to use relation algebras, which are useful for high-level specification and verification, for proving the correctness of lower-level array-based implementations of algorithms. We give a simple relation-algebraic semantics of read and write operations on associative arrays. The array operations seamlessly integrate with assignments in computation models supporting while-programs. As a result, relation algebras can be used for verifying programs with associative arrays. We verify the correctness of an array-based implementation of disjoint-set forests using the union-by-rank strategy and find operations with path compression, path splitting and path halving. All results are formally proved in Isabelle/HOL. This paper is an extended version of [1]. [ABSTRACT FROM AUTHOR]

A successful automated program proof is, in software verification, the ultimate triumph. In practice, however, the road to such success is paved with many failed proof attempts. Unlike a failed test, which provides concrete evidence of an actual bug in the program, a failed proof leaves the programmer in the dark. Can we instead learn something useful from it? The work reported here takes advantage of the rich information that some automatic provers internally collect about the program when attempting a proof. If the proof fails, the Proof2Test tool presented in this article uses the counterexample generated by the prover (specifically, the SMT solver underlying the Boogie tool used in the AutoProof system to perform correctness proofs of contract‐equipped Eiffel programs) to produce a failed test, which provides the programmer with immediately exploitable information to correct the program. The discussion presents Proof2Test and the application of the ideas and tool to a collection of representative examples. [ABSTRACT FROM AUTHOR]

We apply program verification technology to the problem of specifying and verifying automatic differentiation (AD) algorithms. We focus on define-by-run, a style of AD where the program that must be differentiated is executed and monitored by the automatic differentiation algorithm. We begin by asking, "what is an implementation of AD?" and "what does it mean for an implementation of AD to be correct?" We answer these questions both at an informal level, in precise English prose, and at a formal level, using types and logical assertions. After answering these broad questions, we focus on a specific implementation of AD, which involves a number of subtle programming-language features, including dynamically allocated mutable state, first-class functions, and effect handlers. We present a machine-checked proof, expressed in a modern variant of Separation Logic, of its correctness. We view this result as an advanced exercise in program verification, with potential future applications to the verification of more realistic automatic differentiation systems and of other software components that exploit delimited-control effects. [ABSTRACT FROM AUTHOR]

Fault-tolerant algorithms, such as Reliable Broadcast, assure the correct operation of modern distributed systems, even when some of the system nodes fail. However, the development of distributed algorithms is a manual and complex process, where slight changes in requirements can require a complete redesign of the algorithm. To automate the process of developing such algorithms, this work presents a new approach that uses Reinforcement Learning to synthesize correct and efficient fault-tolerant distributed algorithms. This work shows the first application of the approach on the synthesis of fault-tolerant Reliable Broadcast algorithms. The presented technique is capable of synthesizing correct and efficient algorithms with the same performance as others available in the literature as well as a new Byzantine tolerant algorithm, in only 12,000 learning episodes. Based on the success of this implementation, we aim, in the future, to extend this technique to other distributed algorithms such as Consensus.

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. [ABSTRACT FROM AUTHOR]

Smart contract represents an essential application scenario of blockchain technology.Smart contract technology improves programmability and scalability of blockchain, and has broad development prospects.However, a series of security incidents caused a great number of economic losses and weakened users’ confidence in the Ethereum platform.The security of smart contract has become a critical problem that restricts the further development of smart contract.Defects in smart contract code may cause serious consequences and cannot be modified once deployed, it is especially important to verify the correctness of smart contract in advance.In recent years, researchers have obtained many achievements in verification of smart contract, but there is a lack of systematic summary of these research results.Therefore, some basic principles of Ethereum were introduced, including the transaction, gas mechanism, storage and programming language.Eight common types of vulnerabilities in smart contract were summarized and their causes were explained.Some real security events were reviewed and some examples of vulnerability codes were presented.Then, the research work on automatic verification of smart contract based on symbolic execution, model checking and theorem proving was classified and summarized.Three open-source automated tools were selected, including Mythril, Slither and Oyente.And experiments were implemented to evaluate and compare the three tools from the aspects of efficiency, accuracy and the types of vulnerability can be detected.Furthermore, related review articles were surveyed, and the advantages of this paper compared with these works were summarized.The critical problems in the vulnerability detection technology of smart contract were also summarized and the direction of future research was proposed at last.

Correctness-by-Construction (CbC) is an incremental software development technique in the field of formal methods to create functionally correct programs guided by a specification. In contrast to post-hoc verification, where the specification and verification take part after implementing a program, with CbC the specification is defined first, and then the program is successively created using a small set of refinement rules that define side conditions preserving the correctness of the program. This specification-first, refinement-based approach as pursued by CbC has the advantage that errors are likely to be detected earlier in the design process and can be tracked more easily. Even though the idea of CbC emerged over 40 years ago, CbC is not widespread and is mostly used to create small algorithms. We believe in the idea of CbC and envision a scaled CbC approach that contributes to solving problems of modern software verification. In this short paper, we give an overview of our research regarding CbC in four different lines of research. For all of them, we provide tool support for building the CORC ecosystem that even further enables CbC-based development for different fields of application and size of software systems. Furthermore, we give an outlook on future work that extends on our concepts for CbC. [ABSTRACT FROM AUTHOR]

Model-based systems engineering approaches support the early adoption of a model - a collection of abstractions - of the system under development. The system model can be augmented with key properties of the system including formal specifications of system behavior that codify portions of system and unit-level requirements. There are obvious gaps between the model with formally specified behavior and the deployed system. Previous work on component contract languages has shown how behavior can be specified in models defined using the Architecture Analysis and Design Language (AADL) - a SAE International standard (AS5506C). That work demonstrated the effectiveness of model-level formal methods specification and verification but did not provide a strong and direct connection to system implementations developed using conventional programming languages. In particular, there was no refinement of model-level contracts to programming language-level contracts nor a framework for formally verifying that program code conforms to model-level behavioral specifications. To address these gaps and to enable the practical application of model-contract languages for verification of deployed high-integrity systems, this paper describes the design of the GUMBO AADL contract language that integrates and extends key concepts from earlier contract languages. The GUMBO contract language (GCL) is closely aligned to a formal semantics of the AADL run-time framework, which provides a platform- and language-independent specification of AADL semantics. We have enhanced the HAMR AADL code generation framework to translate model-level contracts to programming language-level contracts in the Slang highintegrity language. We demonstrate how the Logika verification tool can automatically verify that Slang-based AADL component implementations conform to contracts, both at the code-level and model-level. Slang-based implementations of AADL systems can be executed directly or compiled to C for deployments on Linux or the seL4 verified microkernel. [ABSTRACT FROM AUTHOR]

Automatically verifying multi-threaded programs is difficult because of the vast number of thread interleavings, a problem aggravated by weak memory consistency. Partial orders can help with verification because they can represent many thread interleavings concisely. However, there is no dedicated decision procedure for solving partial-order constraints. In this article, we propose a novel ordering consistency theory for concurrent program verification that is applicable not only under sequential consistency, but also under the TSO and PSO weak memory models. We further develop an efficient theory solver, which checks consistency incrementally, generates minimal conflict clauses, and includes a custom propagation procedure. We have implemented our approach in a tool, called Zord, and have conducted extensive experiments on the SV-COMP 2020 ConcurrencySafety benchmarks. Our experimental results show a significant improvement over the state-of-the-art. [ABSTRACT FROM AUTHOR]

The theory of arrays has been widely investigated. But concatenation, an operator that consistently appears in specifications of functional-correctness verification tools (e.g., Dafny, VeriFast, VST), is not included in most variants of the theory. Arrays with concatenation need better solvers with theoretical guarantees. We formalize a theory of arrays with concatenation, and define the array property fragment with concatenation. Although the array property fragment without concatenation is decidable, the fragment with concatenation is undecidable in general (e.g., when the base theory for array elements is linear integer arithmetic). But we characterize a “tangle-free” fragment; we present an algorithm that classifies verification goals in the array property fragment with concatenation as tangle-free or entangled, and that decides validity of tangle-free goals. We implement the algorithm in Coq and apply it to functional-correctness verification of C programs. The result shows our algorithm is reasonably efficient and reduces a significant amount of human effort in verification tasks. We also give an algorithm for using this array theory solver as a theory solver in SMT solvers. [ABSTRACT FROM AUTHOR]