Theorem Proving in Higher Order Logics

DOI10.1007/B100400MaRDI QIDQ5464641zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

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

Describes a project that uses

Uses Software

• FRIDGE
• HOL
• Simulink

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)