A Verified Validator for Sparse Sparrow

Getting SparrowBerry »

The analysis design is correct.


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?


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.


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:

  • "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".

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.

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