Abstraction of hardware construction

DOI10.1007/3-540-61254-8_30MaRDI QIDQ4645815zbMATH OpenOpenAlexFDO

Authors Liguo Wang, Michael Mendler

Publication date 11 January 2019

Published in Higher-Order Algebra, Logic, and Term Rewriting (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61254-8_30

zbMATH Keywords

formal verificationtheorem proverconstruction schemespecification schemeconstruction model

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07)

Recommendations

• scientific article; zbMATH DE number 884995
• scientific article; zbMATH DE number 514046
• scientific article; zbMATH DE number 796294
• Abstracting abstract machines
• Abstract Interpretation of the Physical Inputs of Embedded Programs
• Abstract interfaces of input/output logic
• Synthesizable high level hardware descriptions
• Systematic abstraction of abstract machines

Cites work

• scientific article; zbMATH DE number 3991418 (Why is no real title available?)
• scientific article; zbMATH DE number 3991419 (Why is no real title available?)
• scientific article; zbMATH DE number 46617 (Why is no real title available?)
• scientific article; zbMATH DE number 48334 (Why is no real title available?)
• scientific article; zbMATH DE number 139807 (Why is no real title available?)
• scientific article; zbMATH DE number 512956 (Why is no real title available?)
• scientific article; zbMATH DE number 514046 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Correct hardware design and verification methods. IFIP WG10.2 Advanced research working conference, CHARME '93, Arles, France, May 24-26, 1993. Proceedings
• FM8501: a verified microprocessor

Cited in

(1)

• Abstract Interpretation of the Physical Inputs of Embedded Programs

Describes a project that uses

Uses Software

• HOL
• NQTHM

This page was built for publication: Abstraction of hardware construction

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