Formal Methods in Computer-Aided Design

DOI10.1007/B102264MaRDI QIDQ5492965zbMATH OpenOpenAlexFDO

Authors Behzad Akbarpour, Sofiène Tahar

Publication date 20 October 2006

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

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Numerical methods for discrete and fast Fourier transforms (65T50)

Recommendations

• The formalization of discrete Fourier transform in HOL
• scientific article; zbMATH DE number 2102720
• Formalization of fixed-point arithmetic in HOL
• scientific article; zbMATH DE number 2086952
• Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover

Cited in

(11)

• scientific article; zbMATH DE number 1863383 (Why is no real title available?)
• scientific article; zbMATH DE number 2102720 (Why is no real title available?)
• Algebra and Coalgebra in Computer Science
• The correctness of the fast Fourier transform: A structured proof in ACL2
• Unified program generation and verification: a case study on number-theoretic transform
• The formalization of discrete Fourier transform in HOL
• Formalization of transform methods using HOL Light
• Modeling multi-rate DSP specification semantics for formal transformational design in HOL
• Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
• scientific article; zbMATH DE number 2086952 (Why is no real title available?)
• Formalization of fixed-point arithmetic in HOL

Describes a project that uses

Uses Software

• FRIDGE
• HOL Light
• HOL
• Coq
• ACL2

This page was built for publication: Formal Methods in Computer-Aided Design

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