An SMT theory of fixed-point arithmetic

DOI10.1007/978-3-030-51074-9_2OpenAlexW3040611682MaRDI QIDQ2096435

Zvonimir Rakamarić, Shaobo He, Thanh Son Nguyen, Mathias Lechner, Marek Baranowski

Publication date: 9 November 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_2

zbMATH Keywords

SMTdecision procedurefixed-point arithmetic

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

\textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks

Uses Software

• Boolector
• Yices
• z3
• CVC4
• MathSAT5
• PySMT
• BoogiePL
• GitHub
• SMACK
• UppSAT

Cites Work

• Unnamed Item
• Deciding floating-point logic with abstract conflict driven clause learning
• Exploring approximations for floating-point arithmetic using UppSAT
• Reluplex: an efficient SMT solver for verifying deep neural networks
• A three-tier strategy for reasoning about floating-point numbers in SMT
• Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
• Arithmetic Approaches for Rigorous Design of Reliable Fixed-Point LTI Filters
• How Many Bits Does it Take to Quantize Your Neural Network?
• The MathSAT5 SMT Solver
• Learning representations by back-propagating errors

This page was built for publication: An SMT theory of fixed-point arithmetic