A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures

DOI10.1007/s10817-006-9035-0zbMath1113.68091OpenAlexW1992409933MaRDI QIDQ877828

Panagiotis Manolios, Sudarshan K. Srinivasan

Publication date: 3 May 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-006-9035-0

zbMATH Keywords

term-level pipelined machine models

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• ACL2
• Yices
• Siege
• UCLID
• NQTHM

Cites Work

• Functional programming languages and computer architecture, 2nd Conference, Nancy, France, September 16-19, 1985
• Characterizing finite Kripke structures in propositional temporal logic
• Definitional interpreters for higher-order programming languages
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• The Mechanical Evaluation of Expressions
• Correct Hardware Design and Verification Methods
• Correct Hardware Design and Verification Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures