Formal Methods in Computer-Aided Design

DOI10.1007/B102264zbMATH Open1117.68484OpenAlexW4229585471MaRDI QIDQ5492965FDOQ5492965

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

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

Mathematics Subject Classification ID

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

Cited In (11)

• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Formalization of transform methods using HOL Light
• The formalization of discrete Fourier transform in HOL
• 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
• Title not available (Why is that?)
• Formalization of fixed-point arithmetic in HOL

Uses Software

• ACL2
• Coq
• HOL
• HOL Light
• FRIDGE

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)