Sparse Sparrow is a sound, global, yet scalable analyzer for C. The design of Sparse Sparrow is proven correct by the abstract interpretation and the global sparse analysis framework.
However, it does not necessarily mean that the implementation, which has lots of engineering, is also correct conforming to the correct design. Then how to believe analysis results?
Our solution is SparrowBerry, a validator formally verified in Coq. SparrowBerry checks if the analysis result from Sparse Sparrow is indeed a sound abstract semantics of the input C program.
sparrowberry-2.0.1.tar.gz (release date: 16 Nov 2013)
SparrowBerry is distributed under the GNU GPLv3 license.
The source code is compatible with Coq 8.4pl2.
The project is composed of 4 directories:
SparrowBerry succeeded in validating the analysis results of 16 real-world open-source benchmark programs.
Performance of the validator: times (in seconds) and memory consumptions (in megabytes) are represented for all benchmarks with respect to the analyzer and the validator. The performance is evaluated for the analyzer that bugs are fixed by validation. LOC shows the number of lines of code, calculated with "wc". The validator has largely three phases: Trs reports the data translation time. Dns reports the densification time. Lastly, Val reports the time for whole validations, including the prefixed point validation. CmpTime indicates how much the validator is faster than the analyzer. Similarly, CmpMem indicates how less the validator consumes memory than the analyzer.