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.

Citation

BibTeX

@inproceedings{2017_aplas_hr,
  title = {Counterexample-Guided Bit-Precision Selection},
  author = {Shaobo He and Zvonimir Rakamaric},
  booktitle = {Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS)},
  series = {Lecture Notes in Computer Science},
  volume = {10695},
  publisher = {Springer},
  editor = {Bor-Yuh Evan Chang},
  pages = {534--553},
  doi = {10.1007/978-3-319-71237-6_26},
  year = {2017}
}

Acknowledgements

This work was supported in part by NSF awards CNS 1527526 and CCF 1552975.