The OTTER environment for resolution-based proof of hardware correctness

Paolo Camurati; Tiziana Margaria; Paolo Prinetto

doi:10.1016/0165-6074(90)90277-G

The OTTER environment for resolution-based proof of hardware correctness

Paolo Camurati, Tiziana Margaria, Paolo Prinetto

Polytechnic University of Turin

Research output: Contribution to journal › Article › peer-review

Abstract

Efficient proof techniques are vital for the success of formal verification of hardware. First-Order Logic theorem provers satisfy this requirement. This paper deals with experiences in applying such a tool, OTTER, to boolean expression and combinational logic. Preliminary results are reported and future developments are described.

Original language	English
Pages (from-to)	421-428
Number of pages	8
Journal	Microprocessing and Microprogramming
Volume	30
Issue number	1-5
DOIs	https://doi.org/10.1016/0165-6074(90)90277-G
Publication status	Published - Aug 1990
Externally published	Yes

Access to Document

10.1016/0165-6074(90)90277-G

Cite this

@article{9d0bf5d019a549fa8a025516109a4782,

title = "The OTTER environment for resolution-based proof of hardware correctness",

abstract = "Efficient proof techniques are vital for the success of formal verification of hardware. First-Order Logic theorem provers satisfy this requirement. This paper deals with experiences in applying such a tool, OTTER, to boolean expression and combinational logic. Preliminary results are reported and future developments are described.",

author = "Paolo Camurati and Tiziana Margaria and Paolo Prinetto",

year = "1990",

month = aug,

doi = "10.1016/0165-6074(90)90277-G",

language = "English",

volume = "30",

pages = "421--428",

journal = "Microprocessing and Microprogramming",

issn = "0165-6074",

number = "1-5",

}

TY - JOUR

T1 - The OTTER environment for resolution-based proof of hardware correctness

AU - Camurati, Paolo

AU - Margaria, Tiziana

AU - Prinetto, Paolo

PY - 1990/8

Y1 - 1990/8

N2 - Efficient proof techniques are vital for the success of formal verification of hardware. First-Order Logic theorem provers satisfy this requirement. This paper deals with experiences in applying such a tool, OTTER, to boolean expression and combinational logic. Preliminary results are reported and future developments are described.

AB - Efficient proof techniques are vital for the success of formal verification of hardware. First-Order Logic theorem provers satisfy this requirement. This paper deals with experiences in applying such a tool, OTTER, to boolean expression and combinational logic. Preliminary results are reported and future developments are described.

UR - http://www.scopus.com/inward/record.url?scp=0025469492&partnerID=8YFLogxK

U2 - 10.1016/0165-6074(90)90277-G

DO - 10.1016/0165-6074(90)90277-G

M3 - Article

AN - SCOPUS:0025469492

SN - 0165-6074

VL - 30

SP - 421

EP - 428

JO - Microprocessing and Microprogramming

JF - Microprocessing and Microprogramming

IS - 1-5

ER -

The OTTER environment for resolution-based proof of hardware correctness

Abstract

Access to Document

Other files and links

Fingerprint

Cite this