scientific article; zbMATH DE number 2086952

MaRDI QIDQ4737560zbMATH OpenFDO

Authors Behzad Akbarpour, Abdelkader Dekdouk, Sofiène Tahar

Publication date 11 August 2004

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2335/23350185.htm

zbMATH Keywords

HOLSignal ProcessingFixed-pointFloating-pointTheorem-ProvingSPW

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Formalization of fixed-point arithmetic in HOL
• Formal Methods in Computer-Aided Design
• Formal verification of the VAMP floating point unit
• A parameterized floating-point formalizaton in HOL Light
• Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover

Cited in

(4)

• A parameterized floating-point formalizaton in HOL Light
• Formal Methods in Computer-Aided Design
• Error analysis of digital filters using HOL theorem proving
• Formalization of fixed-point arithmetic in HOL

Describes a project that uses

Uses Software

• HOL Light

This page was built for publication:

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