An SMT Theory of Fixed-Point Arithmetic

被引：8

作者：

Baranowski, Marek ^{[1
]}

He, Shaobo ^{[1
]}

Lechner, Mathias ^{[2
]}

Nguyen, Thanh Son ^{[1
]}

Rakamaric, Zvonimir ^{[1
]}

机构：

[1] Univ Utah, Sch Comp, Salt Lake City, UT USA

[2] IST Austria, Klosterneuburg, Austria

来源：

AUTOMATED REASONING, PT I | 2020年 / 12166卷

基金：

奥地利科学基金会;

关键词：

SMT; Fixed-point arithmetic; Decision procedure;

D O I：

10.1007/978-3-030-51074-9_2

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：13 / 31

页数：19

共 50 条

[1] Fixed-Point Arithmetic in FPGA
Becvar, M.
Stukjunger, P.
[J]. ACTA POLYTECHNICA, 2005, 45 (02) : 67 - 72
[2] Massive MIMO in Fixed-Point Arithmetic
Tian, Mi
Sima, Mihai
McGuire, Michael
[J]. 2021 23RD INTERNATIONAL CONFERENCE ON ADVANCED COMMUNICATION TECHNOLOGY (ICACT 2021): ON-LINE SECURITY IN PANDEMIC ERA, 2021, : 91 - 95
[3] Massive MIMO in Fixed-Point Arithmetic
Tian, Mi
Sima, Mihai
McGuire, Michael
[J]. 2022 24TH INTERNATIONAL CONFERENCE ON ADVANCED COMMUNICATION TECHNOLOGY (ICACT): ARITIFLCIAL INTELLIGENCE TECHNOLOGIES TOWARD CYBERSECURITY, 2022, : 91 - 95
[4] Formalization of fixed-point arithmetic in HOL
Akbarpour, B
Tahar, S
Dekdouk, A
[J]. FORMAL METHODS IN SYSTEM DESIGN, 2005, 27 (1-2) : 173 - 200
[5] Simulation of the fixed-point number arithmetic
Wang, Feng
Zheng, Xiaoli
[J]. MATERIALS, MECHATRONICS AND AUTOMATION, PTS 1-3, 2011, 467-469 : 2097 - +
[6] Fixed-point arithmetic line clipping
Mollá, R
Jorquera, P
Vivó, R
[J]. WSCG'2003 POSTER PROCEEDINGS, 2003, : 93 - 96
[7] Formalization of Fixed-Point Arithmetic in HOL
Behzad Akbarpour
Sofiène Tahar
Abdelkader Dekdouk
[J]. Formal Methods in System Design, 2005, 27 : 173 - 200
[8] FIXED-POINT THEORY IN WEAK 2ND-ORDER ARITHMETIC
SHIOJI, N
TANAKA, K
[J]. ANNALS OF PURE AND APPLIED LOGIC, 1990, 47 (02) : 167 - 188
[9] Tight Error Analysis in Fixed-Point Arithmetic
Simic, Stella
Bemporad, Alberto
Inverso, Omar
Tribastone, Mirco
[J]. INTEGRATED FORMAL METHODS, IFM 2020, 2020, 12546 : 318 - 336
[10] A decoder for LVCSR based on fixed-point arithmetic
Bocchieri, Enrico
Blewett, Doug
[J]. 2006 IEEE INTERNATIONAL CONFERENCE ON ACOUSTICS, SPEECH AND SIGNAL PROCESSING, VOLS 1-13, 2006, : 1113 - 1116

← 1 2 3 4 5 →