An SMT theory of fixed-point arithmetic
Baranowski M, He S, Lechner M, Nguyen TS, Rakamarić Z. 2020. An SMT theory of fixed-point arithmetic. Automated Reasoning. IJCAR: International Joint Conference on Automated Reasoning, LNCS, vol. 12166, 13–31.
Download (ext.)
Conference Paper
| Published
| English
Scopus indexed
Author
Baranowski, Marek;
He, Shaobo;
Lechner, MathiasISTA;
Nguyen, Thanh Son;
Rakamarić, Zvonimir
Department
Grant
Series Title
LNCS
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.
Publishing Year
Date Published
2020-06-24
Proceedings Title
Automated Reasoning
Volume
12166
Page
13-31
Conference
IJCAR: International Joint Conference on Automated Reasoning
Conference Location
Paris, France
Conference Date
2020-07-01 – 2020-07-04
ISBN
ISSN
eISSN
IST-REx-ID
Cite this
Baranowski M, He S, Lechner M, Nguyen TS, Rakamarić Z. An SMT theory of fixed-point arithmetic. In: Automated Reasoning. Vol 12166. Springer Nature; 2020:13-31. doi:10.1007/978-3-030-51074-9_2
Baranowski, M., He, S., Lechner, M., Nguyen, T. S., & Rakamarić, Z. (2020). An SMT theory of fixed-point arithmetic. In Automated Reasoning (Vol. 12166, pp. 13–31). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-030-51074-9_2
Baranowski, Marek, Shaobo He, Mathias Lechner, Thanh Son Nguyen, and Zvonimir Rakamarić. “An SMT Theory of Fixed-Point Arithmetic.” In Automated Reasoning, 12166:13–31. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-51074-9_2.
M. Baranowski, S. He, M. Lechner, T. S. Nguyen, and Z. Rakamarić, “An SMT theory of fixed-point arithmetic,” in Automated Reasoning, Paris, France, 2020, vol. 12166, pp. 13–31.
Baranowski M, He S, Lechner M, Nguyen TS, Rakamarić Z. 2020. An SMT theory of fixed-point arithmetic. Automated Reasoning. IJCAR: International Joint Conference on Automated Reasoning, LNCS, vol. 12166, 13–31.
Baranowski, Marek, et al. “An SMT Theory of Fixed-Point Arithmetic.” Automated Reasoning, vol. 12166, Springer Nature, 2020, pp. 13–31, doi:10.1007/978-3-030-51074-9_2.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Link(s) to Main File(s)
Access Level
Open Access
Export
Marked PublicationsOpen Data ISTA Research Explorer
Google Scholar
ISBN Search