SparrowBerry

SparrowBerry
A Verified Validator for Sparse Sparrow

Getting SparrowBerry »

"Sparse Sparrow, Verified!"

The analysis design is correct.

design

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.

Is the implementation correct?

implementation

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?

Check the analysis results with SparrowBerry.

validtion

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.

Getting SparrowBerry

Download

sparrowberry-2.0.1.tar.gz (release date: 16 Nov 2013)

SparrowBerry is distributed under the GNU GPLv3 license.

Composition

The source code is compatible with Coq 8.4pl2.

The project is composed of 4 directories:

  • "coq" contains our formalization.
  • "core" contains the validator code, implemented with OCaml.
  • "dens" contains the densifier code. For details of the densification process, see our publications below.
  • "ext" contains the extracted code from code in "coq".

Publications

Experiments

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.

People

Sungkeun Cho
Jeehoon Kang
Joonwon Choi
Chung-Kil Hur
Kwangkeun Yi

Acknowledgement

This work was supported by the Engineering Research Center of Excellence Program of Korea Ministry of Education, Science and Technology(MEST) / National Research Foundation of Korea(NRF) (Grant 2012-0000468).


ROPAS, Research On Program Analysis System


ROSAEC, Research On Software Analysis for Error-free Computing


SNU, Seoul National University