Symbolic execution is a software verification technique symbolically running programs and thereby checking for bugs. Ranged symbolic execution performs symbolic execution on program parts, so-called path ranges, in parallel. Due to the parallelism, verification is accelerated and hence scales to larger programs. In this paper, we discuss a generalization of ranged symbolic execution to arbitrary program analyses. More specifically, we present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel. Our approach in particular allows to run different analyses on different program parts. We have implemented this generalization on top of the tool CPAchecker and evaluated it on programs from the SV-COMP benchmark. Our evaluation shows that verification can benefit from the parallelization of the verification task, but also needs a form of work stealing (between analyses) to become efficient.

Abstract Cooperative software validation aims at having verification and/or testing tools cooperate on the task of correctness checking. Cooperation involves the exchange of information about currently achieved results in the form of (verification) artifacts. These artifacts are typically specialized to the type of analysis performed by the tool, e.g., bounded model checking, abstract interpretation or symbolic execution, and hence require the definition of a new artifact for every new cooperation to be built. In this article, we introduce a unified artifact (called Generalized Information Exchange Automaton, short GIA) supporting the cooperation of over-approximating with under-approximating analyses. It provides information gathered by an analysis to its partner in a cooperation, independent of the type of analysis and usage context within software validation. We provide a formal definition of this artifact in the form of an automaton together with two operators on GIAs. The first operation reduces a program by excluding these parts, where the information that they are already processed is encoded in the GIA. The second operation combines partial results from two GIAs into a single on. We show that computed analysis results are never lost when connecting tools via these operations. To experimentally demonstrate the feasibility, we have implemented two such cooperation: one for verification and one for testing. The obtained results show the feasibility of our novel artifact in different contexts of cooperative software validation, in particular how the new artifact is able to overcome some drawbacks of existing artifacts.

Abstract Ranged symbolic execution has been proposed as a way of scaling symbolic execution by splitting the task of path exploration onto several workers running in parallel. The split is conducted along path ranges which – simply speaking – describe sets of paths. Workers can then explore path ranges in parallel. In this paper, we propose ranged analysis as the generalization of ranged symbolic execution to arbitrary program analyses. This allows us to not only parallelize a single analysis, but also run different analyses on different ranges of a program in parallel. Besides this generalization, we also provide a novel range splitting strategy operating along loop bounds, complementing the existing random strategy of the original proposal. We implemented ranged analysis within the tool CPAchecker and evaluated it on programs from the SV-COMP benchmark. The evaluation in particular shows the superiority of loop bounds splitting over random splitting. We furthermore find that compositions of ranged analyses can solve analysis tasks that none of the constituent analysis alone can solve.

Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software verification might find their way into practice faster if provided in smaller, more specialized components.

Software verification is the task of proving correct-ness of programs against specified requirements. Key to software verification is the automatic generation of loop invariants. In recent years, template- and logic-based approaches to invariant generation have been complemented by machine learning (ML) techniques. A number of proposals for such techniques exist today. Although all authors perform experimental evaluations of their proposals, comparability of the core techniques is nev-ertheless hindered by differing benchmarks, specific tunings of hyperparameters, missing public availability as well as specialized preprocessings and runtime environments. In this paper, we present the modular framework MIGMLfor experimentation with and comparison of ML invariant generators. MIGMLcontains the core ingredients of ML based invariant generators (i.e. a teacher and a learner) as instantiable components with clear-cut interfaces. This conceptually novel framework allows for a reproducibility study of four existing ML invariant generators: we re-implement the teacher and learner components of the four techniques within our framework which permits a comparison on equal grounds. We are able to successfully reproduce and partially confirm the reported results. We furthermore experiment with novel combinations of components, e.g. employ the data generator within the teacher of technique A together with the learner of technique B. As a result, we observe that such combinations can lead to an overall enhanced effectiveness.

Debugging, that is, identifying and fixing bugs in software, is a central part of software development. Developers are therefore often confronted with the task of deciding whether a given code snippet contains a bug, and if yes, where. Recently, data-driven methods have been employed to learn this task of bug detection, resulting (amongst others) in so called neural bug detectors. Neural bug detectors are trained on millions of buggy and correct code snippets.

Abstract Software verification has recently made enormous progress due to the development of novel verification methods and the speed-up of supporting technologies like SMT solving. To keep software verification tools up to date with these advances, tool developers keep on integrating newly designed methods into their tools, almost exclusively by re-implementing the method within their own framework. While this allows for a conceptual re-use of methods, it nevertheless requires novel implementations for every new technique. In this paper, we employ cooperative verification in order to avoid re-implementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for the core ingredient of software verification which is invariant generation. Finding an adequate loop invariant is key to the success of a verification run. Our framework named CoVEGI allows a master verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators. Their results are then utilized within the verification run of the master verifier, allowing in particular for crosschecking the validity of the invariant. We experimentally evaluate our framework on an instance with two masters and three different invariant generators using a number of benchmarks from SV-COMP 2020. The experiments show that the use of CoVEGI can increase the number of correctly verified tasks without increasing the used resources.

We present CLARC (Cryptographic Library for Anonymous Reputation and Credentials), an anonymous credentials system (ACS) combined with an anonymous reputation system.