Modeling a hardware synthesis methodology in Isabelle

DOI10.1007/BFB0105395MaRDI QIDQ6567702zbMATH OpenFDO

Authors David Basin, Stefan Friedrich

Publication date 5 July 2024

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• scientific article; zbMATH DE number 2084337
• scientific article; zbMATH DE number 2185688
• Geometry of synthesis: a structured approach to VLSI design
• scientific article; zbMATH DE number 1507239
• Proof producing synthesis of arithmetic and cryptographic hardware

Cites work

• Isabelle. A generic theorem prover

Cited in

(1)

• Implementation issues about the embedding of existing high level synthesis algorithms in HOL

This page was built for publication: Modeling a hardware synthesis methodology in Isabelle

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