Error analysis of digital filters using HOL theorem proving

DOI10.1016/j.jal.2006.11.001zbMath1133.68422OpenAlexW2075202684MaRDI QIDQ2475434

Sofiène Tahar, Behzad Akbarpour

Publication date: 11 March 2008

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2006.11.001

zbMATH Keywords

digital filterstheorem provingerror analysisfixed-pointHOLfloating-point

Mathematics Subject Classification ID

Uses Software

• ML
• Simulink
• HOL
• HOL Light
• FRIDGE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formalization of fixed-point arithmetic in HOL
• A Skeptic's approach to combining HOL and Maple
• Constructing the real numbers in HOL
• Floating-Point-Roundoff Accumulation in Digital-Filter Realizations

This page was built for publication: Error analysis of digital filters using HOL theorem proving