Formalization of fixed-point arithmetic in HOL

DOI10.1007/s10703-005-2256-8zbMath1085.68148OpenAlexW1967747780MaRDI QIDQ816219

Sofiène Tahar, Behzad Akbarpour, Abdelkader Dekdouk

Publication date: 20 February 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://spectrum.library.concordia.ca/977379/1/FMSD-2005.pdf

zbMATH Keywords

theorem provingfloating-point arithmeticHOLfixed-point arithmetic

Mathematics Subject Classification ID

Related Items (2)

Formalization of linear space theory in the higher-order logic proving system ⋮ Error analysis of digital filters using HOL theorem proving

Uses Software

• ACL2
• ML
• Simulink
• HOL
• HOL Light
• SystemC
• FRIDGE

Cites Work

• Constructing the real numbers in HOL
• Correct Hardware Design and Verification Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalization of fixed-point arithmetic in HOL