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

DOI10.1007/BF01384049zbMath0800.68561OpenAlexW2003565260MaRDI QIDQ1329091

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

algebraic specificationhardware verificationOBJ3hardware specificationGordon's computer

Mathematics Subject Classification ID

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

Uses Software

• Unnamed Item
• OBJ3
• 2OBJ
• RRL
• Tecton

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Refutational theorem proving using term-rewriting systems
• Report on the Larch shared language
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• FM8501: a verified microprocessor
• An overview of the Tecton proof system
• The ``Hoare Logic of CSP, and All That
• A logic of authentication

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