An SMT theory of fixed-point arithmetic

DOI10.1007/978-3-030-51074-9_2MaRDI QIDQ2096435zbMATH OpenOpenAlexFDO

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

Publication date 9 November 2022

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

zbMATH Keywords

decision procedurefixed-point arithmeticSMT

Mathematics Subject Classification ID

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

Cites work

• A three-tier strategy for reasoning about floating-point numbers in SMT
• Arithmetic Approaches for Rigorous Design of Reliable Fixed-Point LTI Filters
• Deciding floating-point logic with abstract conflict driven clause learning
• Exploring approximations for floating-point arithmetic using UppSAT
• Formal verification of piece-wise linear feed-forward neural networks
• How many bits does it take to quantize your neural network?
• scientific article; zbMATH DE number 5613976 (Why is no real title available?)
• Learning representations by back-propagating errors
• Reluplex: an efficient SMT solver for verifying deep neural networks
• The MathSAT5 SMT solver

Cited in

(3)

• scientific article; zbMATH DE number 7023675 (Why is no real title available?)
• Multigrid methods using block floating point arithmetic
• \textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2096435)