During the last decade we have developed the Klever software verification framework intended for verification of large critical industrial C programs like operating system kernels. Thanks to developers of automatic software verification tools (primarily CPAchecker) we could demonstrate good enough results, e.g. here is the list of bugs found by Klever in the Linux kernel and acknowledged by the developers. From the other side it became clear that thorough checking of target programs requires considerable investments in studying program environments and requirements as well as development of corresponding models and specifications. In this talk we will present related challenges and preliminary ideas how one can cope with them. Our next talks will elaborate on the most crucial topics.

One of the key problems that can be solved with the Klever software verification framework is thorough verification of a specific software system or its component. Insufficient scalability of employed verification tools may hinder the verification process. The environment model decomposition is a new technique that allows verifying industrial software piecewise in a semi-automatic manner. Its key idea is to develop a single specification for the whole program or program fragment but verify it with different environment models. Such models lead the verification tool to specific places in the program, directly avoiding too many behavioral possibilities in each separate verification task. As a result, the user gets a much better-scaled verification process and a nice list of verdicts for different scenarios of the program behavior verified.

Software verification techniques exchange information to to become more effective and efficient or to increase the trust in the verification result. One information that is to exchanged is precision level of an analysis. So far, precisions are exchanged in the context of regression verification and only between the same analysis. In this talk, we suggest various options to exchange the predicate precision between predicate and value analysis. We discuss our evaluation results for the different exchange options applied to three scenarios, namely, cooperative verification, result validation, and regression verification. Furthermore, we report on comparisons with state-of-the-art techniques for the respective scenarios. To this end, we looked at conditional model checking, witness validation, and the original precision reuse approach.

Understanding of CPAchecker analysis timeouts is extremely hard. For this purpose CPAchecker provides statistics and code coverage reports. We propose to enrich code coverage reports by CPA-state information on SMGCPA example.

Code coverage reports are indispensable for users who want to ensure a great quality of verification results. Indeed, some paths in target programs may remain unexplored due to currently incomplete models of their environments. Code coverage reports can help to identify corresponding places very efficiently. Also, they come to the aid when one needs to reveal those parts of target programs that are most complicated for verification tools. This is possible when verification tool developers enrich standard code coverage reports with additional data. CPAchecker does that. In this talk I will present results of the joint work devoted to representation of CPAchecker’s code coverage reports within the Klever software verification framework. In addition, we will go over a couple of real examples.

Development teams are integrating formal methods in their software-development workflow. For continuous integration, it is mandatory to have checks with a short response time. State-of-the-art frameworks and setups for comparative evaluation have mostly considered execution of tools on dedicated compute clusters such as StarExec or the VerifierCloud. Those executions are however limited in their parallelism by the number of available processing units. Since recent years, large cloud service providers such as Amazon Web Services (AWS) or Microsoft Azure have emerged on the market, providing users with massively parallel computing infrastructures. In this talk I will present a portfolio algorithm implemented in CPAchecker, an approach in which this verifier aims to exploit the availability of exactly such a setting.

CEGAR is a well-known and widely used schema in software verification. Although having this general schema, each tool implements its own CEGAR loop. With our strict decomposition of CEGAR into three loosely coupled components communicating via clearly defined interfaces, we propose a solution to that problem. Providing both a formal definition of the components and interfaces as well as an implementation based on CoVeriTeam and the CPAchecker allows to build a new CEGAR-based tool without reimplementing the whole loop.

Memory safety verification by SMGCPA provides good results on Linux kernel sources with the help of Klever project. Current version of SMGCPA provides a verdict for almost 2/3 of Linux modules, but it seems that the SMG algorithm has a bottleneck in stop/join operations, which prevents analysis of the last 1/3. This talk introduces plans for development of a CEGAR implementation of SMG with a recheck of counterexamples for different assurance in discovery of error.

Over the years, different program transformations have been integrated in CPAchecker: generation of residual programs, program slicing, program simplifications, program mutations, and more. This talk will not present new research results, but give an overview on some of these transformations and how the existing infrastructure can be leveraged for new research.