Abstract

A number of static checking techniques is based on constructing and refining an abstract reachability tree (ART) and reasoning about Linear Arithmetics. For example, in BLAST, each program statement is represented as a series of assignments of a linear functions to variables, and the procedure of predicate discovery relies on Craig interpolation of linear arithmetics and equality with uninterpreted function symbols.

This approach requires implementing operations with higher-level types (lists, sets, maps) in terms of linear arithmetics and if-statements. However, the ART being constructed splits into two branches at each conditional operator, thus expanding exponentially as the number of such operations used grows.

In this paper we propose an approach to extend the domain of mathematical operations a checker described can reason about with the certain operations with finite sets: adding and removing elements, testing whether set contains a particular element, or is empty. It being implemented, the ART doesn’t split at each operation, and no modification is required to LA+EUF interpolation. The tradeoff of it is more complex formulas for a solver to handle.

Performance evaluations demonstrate that the approach proposed, however, doesn’t provide greater scalability than the existing methods due to interploation failures.

The paper and the slides

On this page are presented some materials for my presentation of my paper at SYRCoSE 2010.

Paper: On Reasoning about Finite Sets in Software Model Checking (pdf)

This archive contains the slides. If you want to review presentation or to make a derivative work, it will be useful. The work is in public domain, and you may use certain parts (the pics that demonstrate CEGAR, for example). I am sure that you'll draw the line between "using pics" and "plagiarism" correctly.

The research

Here's a package (439 Kb) with source code of the implementation, and some test source files.

During the talk, I might have referred to a draft of my Masters Thesis. It contains a more formal definition of what finite sets are, as well as a proof of correctness of path formula building algorithms. As the paper will be ready, this reference will be replaced with the one to the final version.

Also I published all materials that concern the experiments carried out during the research. The archive with the tests is above, and the source code of the modified version of BLAST used to carry on experiments is here

Some references

Home page of the BLAST project

LDV program, within which the research was conducted

Clarke's article about CEGAR.