Gordon's computer: A hardware verification case study in OBJ3

DOI10.1007/BF01384049MaRDI QIDQ1329091zbMATH OpenOpenAlexFDO

Authors Victoria Stavridou

Publication date 29 June 1994

Published in Formal Methods in System Design (Search for Journal in Brave)

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

zbMATH Keywords

hardware verificationalgebraic specificationOBJ3hardware specificationGordon's computer

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Fault detection; testing in circuits and networks (94C12) Abstract data types; algebraic specification (68Q65)

Cites work

• scientific article; zbMATH DE number 3821084 (Why is no real title available?)
• scientific article; zbMATH DE number 3978367 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 53982 (Why is no real title available?)
• scientific article; zbMATH DE number 139806 (Why is no real title available?)
• scientific article; zbMATH DE number 139966 (Why is no real title available?)
• scientific article; zbMATH DE number 732939 (Why is no real title available?)
• A logic of authentication
• An overview of the Tecton proof system
• FM8501: a verified microprocessor
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Refutational theorem proving using term-rewriting systems
• Report on the Larch shared language
• The ``Hoare Logic of CSP, and All That

Describes a project that uses

Uses Software

• Tecton
• RRL
• 2OBJ
• OBJ3
• LARCH

This page was built for publication: Gordon's computer: A hardware verification case study in OBJ3

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