Theorem Proving in Higher Order Logics

DOI10.1007/B100400zbMATH Open1099.68719OpenAlexW2798038182MaRDI QIDQ5464641FDOQ5464641

Authors: Behzad Akbarpour, Sofiène Tahar 

Publication date: 18 August 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b100400

Recommendations

• Error analysis of digital filters using HOL theorem proving
• A Coq formalization of digital filters
• A bit too precise? Bounded verification of quantized digital filters
• Computer Aided Verification
• Formalization of fixed-point arithmetic in HOL

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (7)

• Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections
• Error analysis of digital filters using HOL theorem proving
• An error analysis for 2-D block implemented digital filters
• A Coq formalization of digital filters
• A separation theorem for finite precision digital filters
• A bit too precise? Bounded verification of quantized digital filters
• Computer Aided Verification

Uses Software

• Simulink
• HOL
• FRIDGE

This page was built for publication: Theorem Proving in Higher Order Logics

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