scientific article; zbMATH DE number 2086952

zbMATH Open1057.68677MaRDI QIDQ4737560FDOQ4737560

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

Title of this publication is not available (Why is that?)

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

zbMATH Keywords

HOLSignal ProcessingFixed-pointFloating-pointTheorem-ProvingSPW

Mathematics Subject Classification ID

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

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

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)