We address the problem of verifying k-safety properties: properties that refer to k interacting executions of a program. A prominent way to verify k-safety properties is by self composition. In this approach, the problem of checking k-safety over the original program is reduced to checking an “ordinary” safety property over a program that executes k copies of the original program in some order. The way in which the copies are composed determines how complicated it is to verify the composed program. We view this composition as provided by a semantic self composition function that maps each state of the composed program to the copies that make a move. Since the “quality” of a self composition function is measured by the ability to verify the safety of the composed program, we formulate the problem of inferring a self composition function together with the inductive invariant needed to verify safety of the composed program, where both are restricted to a given language. We develop a property-directed inference algorithm that, given a set of predicates, infers composition-invariant pairs expressed by Boolean combinations of the given predicates, or determines that no such pair exists. We implemented our algorithm and demonstrate that it is able to find self compositions that are beyond reach of existing tools.
Equivalence checking is another closely related research field, where a composition of several programs is considered. As an example, equivalence checking is applied to verify the correctness of compiler optimizations @cite_13 @cite_15 @cite_10 @cite_11 . @cite_15 the composition is determined by a brute-force search for possible synchronization points. While this brute-force search resembles our approach for finding the correct composition, it is not guided by the verification process. The works in @cite_10 @cite_11 identify possible synchronization points syntactically, and try to match them during the construction of a simulation relation between programs.
@cite_10 @cite_15 @cite_13 @cite_11
2771024256 1587844310 2810373436
Equivalence checking is an important building block for program synthesis and verification. For a synthesis tool to compete with modern compilers, its equivalence checker should be able to verify the transformations produced by these compilers. We find that the transformations produced by compilers are much varied and the presence of undefined behaviour allows them to produce even more aggressive optimizations. Previous work on equivalence checking has been done in the context of translation validation, where either a pass-by-pass based approach was employed or a set of handpicked optimizations were proven. These settings are not suitable for a synthesis tool where a black-box approach is required. The paper presents a deductive framework for proving program equivalence and its application to automatic verification of transformations performed by optimizing compilers. To leverage existing program analysis techniques, we reduce the equivalence checking problem to analysis of one system --- a cross-product of the two input programs. We show how the approach can be effectively used for checking equivalence of consonant (i.e., structurally similar) programs. Finally, we report on the prototype tool that applies the developed methodology to verify that a compiler optimization run preserves the program semantics. Unlike existing frameworks, CoVaC accommodates absence of compiler annotations and handles most of the classical intraprocedural optimizations such as constant folding, reassociation, common subexpression elimination, code motion, dead code elimination, branch optimizations, and others. Program equivalence checking is a fundamental problem in computer science with applications to translation validation and automatic synthesis of compiler optimizations. Contemporary equivalence checkers employ SMT solvers to discharge proof obligations generated by their equivalence checking algorithm. Equivalence checkers also involve algorithms to infer invariants that relate the intermediate states of the two programs being compared for equivalence. We present a new algorithm, called invariant-sketching, that allows the inference of the required invariants through the generation of counter-examples using SMT solvers. We also present an algorithm, called query-decomposition, that allows a more capable use of SMT solvers for application to equivalence checking. Both invariant-sketching and query-decomposition help us prove equivalence across program transformations that could not be handled by previous equivalence checking algorithms.