Modeling a hardware synthesis methodology in Isabelle

DOI10.1007/BFB0105395zbMATH Open1543.68191MaRDI QIDQ6567702FDOQ6567702

Authors: David Basin, Stefan Friedrich 

Publication date: 5 July 2024

Recommendations

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

Mathematics Subject Classification ID

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

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)