A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
type: Item
instance of: scholarly article
title: A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
zbMATH Open document ID: 1113.68091
author: Panagiotis Manolios
author: Sudarshan K. Srinivasan
published in: Journal of Automated Reasoning
publication date: 2007-05-03T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5149171
zbMATH Keywords: term-level pipelined machine models
describes a project that uses: UCLID
describes a project that uses: Siege
describes a project that uses: ACL2
describes a project that uses: NQTHM
describes a project that uses: Yices
MaRDI profile type: Publication
full work available at URL: s10817-006-9035-0
OpenAlex ID: W1992409933
cites work: Q2729088
cites work: Computer Aided Verification
cites work: Q3835049
cites work: Characterizing finite Kripke structures in propositional temporal logic
cites work: Q4818814
cites work: Q4804887
cites work: Q4817532
cites work: Functional programming languages and computer architecture, 2nd Conference, Nancy, France, September 16-19, 1985
cites work: Q4427901
cites work: The Mechanical Evaluation of Expressions
cites work: Correct Hardware Design and Verification Methods
cites work: Q3992568
cites work: Definitional interpreters for higher-order programming languages
cites work: A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
DOI: 10.1007/S10817-006-9035-0
description: scientific article; zbMATH DE number 5149171