Counterexample-Guided Bit-Precision Selection

Share

Shaobo He, Zvonimir Rakamaric. 15th Asian Symposium on Programming Languages and Systems (APLAS 2017), Suzhou, China.
[pdf] [bib]

Abstract: Static program verifiers based on satisfiability modulo theories (SMT) solvers often trade precision for scalability to be able to handle large programs. A popular trade-off is to model bitwise operations, which are expensive for SMT solving, using uninterpreted functions over integers. Such an over-approximation improves scalability, but can introduce undesirable false alarms in the presence of bitwise operations that are common in, for example, low-level systems software. In this paper, we present our approach to diagnose the spurious counterexamples caused by this trade-off, and leverage the learned information to lazily and gradually refine the precision of reasoning about bitwise operations in the whole program. Our main insight is to employ a simple and fast type analysis to transform both a counterexample and program into their more precise versions that block the diagnosed spurious counterexample. We implement our approach in the SMACK software verifier, and evaluate it on the benchmark suite from the International Competition on Software Verification (SV-COMP). The evaluation shows that we significantly reduce the number of false alarms while maintaining scalability.

Bibtex:

@inproceedings{aplas2017-hr,
  author = {Shaobo He and Zvonimir Rakamari\'c},
  title = {Counterexample-Guided Bit-Precision Selection},
  booktitle = {Proceedings of the 15th Asian Symposium on Programming
    Languages and Systems (APLAS)},
  year = {2017},
  note = {to appear},
}