Algebraic models of correctness for abstract pipelines

No abstract is available for this paper.

• Publication year

  2003

• Venue

  J. Log. Algebraic Methods Program.

• Publication date

  2003-09-01

• Fields of study

  Mathematics, Computer Science, Engineering

• Identifiers
  DOI 10.1016/S1567-8326(03)00041-9
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A Correctness Model for Pipelined Microprocessors

  2005influential reference
• Maude: specification and programming in rewriting logic

  2002cited by this paper
• Prospects for Hardware Foundations

  2002cited by this paper
• Microarchitecture Verification by Compositional Model Checking

  2001cited by this paper
• An algebraic framework for modelling and verifying microprocessors using HOL

  2001cited by this paper
• Verifying a Simple Pipelined Microprocessor Using Maude

  2001cited by this paper
• A Framework for Microprocessor Correctness Statements

  2001cited by this paper
• A HOL specification of the ARM instruction set architecture

  2001cited by this paper
• Verifying Advanced Microarchitectures that Support Speculation and Exceptions

  2000cited by this paper
• Microprocessor Design Verification

  2000cited by this paper
• Hardware Modeling Using Function Encapsulation

  2000cited by this paper
• Algebraic Models of Correctness for Microprocessors

  2000cited by this paper
• Formal Verification of VLIW Microprocessors with Speculative Execution

  2000cited by this paper
• Correctness of Pipelined Machines

  2000cited by this paper
• Correctness and Verification of Hardware Systems Using Maude

  2000cited by this paper
• Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions

  1999cited by this paper
• Processor Verification with Precise Exeptions and Speculative Execution

  1998cited by this paper
• Specifying superscalar microprocessors in Hawk

  1998cited by this paper
• A Correctness Proof of a Speculative, Superscalar, Out-of-Order, Renaming Microarchitecture

  1998cited by this paper
• Formal Verification of Out-of-Order Execution Using Incremental Flushing

  1998cited by this paper
• Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution

  1998cited by this paper
• Algebraic Models of Superscalar Microprocessor Implementations: A Case Study

  1998cited by this paper
• Decomposing the Proof of Correctness of pipelined Microprocessors

  1998cited by this paper
• Systematic formal verification of interpreters

  1997cited by this paper
• Techniques for verifying superscalar microprocessors

  1996cited by this paper
• Mechanically Checking a Lemma Used in an Automatic Verification Tool

  1996cited by this paper
• Inverting the Abstraction Mapping: A Methodology for Hardware Verification

  1996cited by this paper
• Automatic Generation of Invariants in Processor Verification

  1996cited by this paper
• An algebraic approach to syntax, semantics and compilation

  1996cited by this paper
• An Algebraic Model of Correctness for Superscalar Microprocessors

  1996influential reference
• Formal Verification of an Avionics Microprocessor

  1995cited by this paper
• Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods

  1995cited by this paper
• Automatic verification of Pipelined Microprocessor Control

  1994cited by this paper
• FM8501: A Verified Microprocessor

  1994cited by this paper
• Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics

  1994cited by this paper
• A Correctness Model for Pipelined Multiprocessors

  1994influential reference
• Higher Order Logic and Hardware Verification

  1993cited by this paper
• A Theory of Generic Interpreters

  1993cited by this paper
• DDD-FM9001: Derivation of a Verified Microprocessor

  1993cited by this paper
• Universal algebra

  1993cited by this paper
• Designing chips that work

  1992cited by this paper
• The Secd Microprocessor: A Verification Case Study

  1992cited by this paper
• A formal HDL and its use in the FM9001 verification

  1992cited by this paper
• Occam in the specification and verification of microprocessors

  1992cited by this paper
• Universal Algebra for Computer Scientists

  1992cited by this paper
• Mechanized reasoning and hardware design

  1992cited by this paper
• Theoretical Foundations of VLSI Design

  1991cited by this paper
• VERIFYING SECD IN HOL

  1991cited by this paper
• Algebraic Specification

  1991cited by this paper
• Handbook Of Theoretical Computer Science Volume B Formal Models And Semantics

  1990cited by this paper
• Formal verification of a pipelined microprocessor

  1990cited by this paper
• Handbook of theoretical computer science - Part A: Algorithms and complexity; Part B: Formal models and semantics

  1990cited by this paper
• Formal Verification and Implementation of a Microprocessor

  1988cited by this paper
• A Proof of Correctness of the Viper Microprocessor: The First Level

  1988cited by this paper
• Fundamentals of Algebraic Specification 1: Equations and Initial Semantics

  1985cited by this paper
• Proving a computer correct with the LCF_LSM hardware verification system

  1983cited by this paper
• Computer Architecture: A Quantitative Approach

  1969cited by this paper
• The Mechanical Evaluation of Expressions

  1964cited by this paper

• Improvement of Algebraic Models of Abstract Pipelines for Formal Verification

  2018cites this paper
• The data type of spatial objects

  2013influential citation
• Parametric architectures for scientific computing in integrable spaces. The convolution operation as a case of study

  2010cites this paper
• Unifying computers and dynamical systems using the theory of synchronous concurrent algorithms

  2009cites this paper
• Maurer computers for pipelined instruction processing†

  2008cites this paper
• Algebraic models of behaviour and correctness of SMT and CMT processors

  2007cites this paper
• Modelling SMT and CMT Processors : A Simple Case Study DRAFT

  2007cites this paper
• Algebraic Models of Simultaneous Multithreaded and Multi-core Processors

  2007cites this paper
• Algebraic Models of Simultaneous Multi-Threaded and multi-core

  2007influential citation
• Algebraic Model of an Arithmetic Unit for TTE-Computable Normalized Rational Numbers

  2007cites this paper
• Algebraic Models of Simultaneous Multi-Threaded and multi-core Microprocessor

  2007cites this paper
• The Role of Algebraic Models and Type-2 Theory of Effectivity in Special Purpose Processor Design

  2006cites this paper
• Synchronization-at-Retirement for Pipeline Verification

  2004cites this paper
• Formal Specification and Verification of ARM 6

  year unknowncites this paper