Abstract

Fixed-point arithmetic is a popular alternative to floating-point arithmetic on embedded systems. Existing work on the verification of fixed-point programs relies on custom formalizations of fixed-point arithmetic, which makes it hard to compare the described techniques or reuse the implementations. In this paper, we address this issue by proposing and formalizing an SMT theory of fixed-point arithmetic. We present an intuitive yet comprehensive syntax of the fixed-point theory, and provide formal semantics for it based on rational arithmetic. We also describe two decision procedures for this theory: one based on the theory of bit-vectors and the other on the theory of reals. We implement the two decision procedures, and evaluate our implementations using existing mature SMT solvers on a benchmark suite we created. Finally, we perform a case study of using the theory we propose to verify properties of quantized neural networks.

Citation

Marek Baranowski, Shaobo He, Mathias Lechner, Thanh Son Nguyen, Zvonimir Rakamaric
An SMT Theory of Fixed-Point Arithmetic
Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR), 12166: 13--31, doi:10.1007/978-3-030-51074-9_2, 2020.

BibTeX

@inproceedings{2020_ijcar_bhlnr,
  title = {An SMT Theory of Fixed-Point Arithmetic},
  author = {Marek Baranowski and Shaobo He and Mathias Lechner and Thanh Son Nguyen and Zvonimir Rakamaric},
  booktitle = {Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR)},
  series = {Lecture Notes in Computer Science},
  volume = {12166},
  publisher = {Springer},
  editor = {Nicolas Peltier and Viorica Sofronie-Stokkermans},
  pages = {13--31},
  doi = {10.1007/978-3-030-51074-9_2},
  year = {2020}
}

Acknowledgements

This work was supported in part by NSF awards CCF 1552975, CCF 1704715, and the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).

Resources

Videos

An SMT Theory of Fixed-Point Arithmetic