---
_id: '8194'
abstract:
- lang: eng
  text: '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.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
  full_name: Baranowski, Marek
  last_name: Baranowski
- first_name: Shaobo
  full_name: He, Shaobo
  last_name: He
- first_name: Mathias
  full_name: Lechner, Mathias
  id: 3DC22916-F248-11E8-B48F-1D18A9856A87
  last_name: Lechner
- first_name: Thanh Son
  full_name: Nguyen, Thanh Son
  last_name: Nguyen
- first_name: Zvonimir
  full_name: Rakamarić, Zvonimir
  last_name: Rakamarić
citation:
  ama: 'Baranowski M, He S, Lechner M, Nguyen TS, Rakamarić Z. An SMT theory of fixed-point
    arithmetic. In: <i>Automated Reasoning</i>. Vol 12166. Springer Nature; 2020:13-31.
    doi:<a href="https://doi.org/10.1007/978-3-030-51074-9_2">10.1007/978-3-030-51074-9_2</a>'
  apa: 'Baranowski, M., He, S., Lechner, M., Nguyen, T. S., &#38; Rakamarić, Z. (2020).
    An SMT theory of fixed-point arithmetic. In <i>Automated Reasoning</i> (Vol. 12166,
    pp. 13–31). Paris, France: Springer Nature. <a href="https://doi.org/10.1007/978-3-030-51074-9_2">https://doi.org/10.1007/978-3-030-51074-9_2</a>'
  chicago: Baranowski, Marek, Shaobo He, Mathias Lechner, Thanh Son Nguyen, and Zvonimir
    Rakamarić. “An SMT Theory of Fixed-Point Arithmetic.” In <i>Automated Reasoning</i>,
    12166:13–31. Springer Nature, 2020. <a href="https://doi.org/10.1007/978-3-030-51074-9_2">https://doi.org/10.1007/978-3-030-51074-9_2</a>.
  ieee: M. Baranowski, S. He, M. Lechner, T. S. Nguyen, and Z. Rakamarić, “An SMT
    theory of fixed-point arithmetic,” in <i>Automated Reasoning</i>, Paris, France,
    2020, vol. 12166, pp. 13–31.
  ista: '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.'
  mla: Baranowski, Marek, et al. “An SMT Theory of Fixed-Point Arithmetic.” <i>Automated
    Reasoning</i>, vol. 12166, Springer Nature, 2020, pp. 13–31, doi:<a href="https://doi.org/10.1007/978-3-030-51074-9_2">10.1007/978-3-030-51074-9_2</a>.
  short: M. Baranowski, S. He, M. Lechner, T.S. Nguyen, Z. Rakamarić, in:, Automated
    Reasoning, Springer Nature, 2020, pp. 13–31.
conference:
  end_date: 2020-07-04
  location: Paris, France
  name: 'IJCAR: International Joint Conference on Automated Reasoning'
  start_date: 2020-07-01
date_created: 2020-08-02T22:00:59Z
date_published: 2020-06-24T00:00:00Z
date_updated: 2023-08-22T08:27:25Z
day: '24'
department:
- _id: ToHe
doi: 10.1007/978-3-030-51074-9_2
external_id:
  isi:
  - '000884318000002'
intvolume: '     12166'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1007/978-3-030-51074-9_2
month: '06'
oa: 1
oa_version: Published Version
page: 13-31
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: Automated Reasoning
publication_identifier:
  eissn:
  - '16113349'
  isbn:
  - '9783030510732'
  issn:
  - '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: An SMT theory of fixed-point arithmetic
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 12166
year: '2020'
...