Resolution-based correctness proofs of synchronous circuits

Paolo Camurati; Tiziana Margaria; Paolo Prinetto

Resolution-based correctness proofs of synchronous circuits

Paolo Camurati, Tiziana Margaria, Paolo Prinetto

Polytechnic University of Turin

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

First-Order theorem provers like OTTER satisfy the vital need for versatility and efficiency in formal verification of correctness. This paper deals with experiences in applying OTTER to synchronous circuits. Synchronous circuits are first modeled, then proved correct by means of demodulation- and hyperresolution-based methodologies. Experimental examples are discussed, results are reported and a first comparison is drawn with other proof styles.

Original language	English
Title of host publication	Proc Eur Conf Des Autom
Publisher	Publ by IEEE
Pages	11-15
Number of pages	5
ISBN (Print)	0818626453
Publication status	Published - 1992
Externally published	Yes
Event	Proceedings the European Conference on Design Automation - Amsterdam, Neth Duration: 16 Mar 1992 → 19 Mar 1992

Publication series

Name	Proc Eur Conf Des Autom

Conference

Conference	Proceedings the European Conference on Design Automation
City	Amsterdam, Neth
Period	16/03/92 → 19/03/92

Cite this

@inproceedings{4982c41762dd43a293dcab0d7a1db66d,

title = "Resolution-based correctness proofs of synchronous circuits",

abstract = "First-Order theorem provers like OTTER satisfy the vital need for versatility and efficiency in formal verification of correctness. This paper deals with experiences in applying OTTER to synchronous circuits. Synchronous circuits are first modeled, then proved correct by means of demodulation- and hyperresolution-based methodologies. Experimental examples are discussed, results are reported and a first comparison is drawn with other proof styles.",

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

year = "1992",

language = "English",

isbn = "0818626453",

series = "Proc Eur Conf Des Autom",

publisher = "Publ by IEEE",

pages = "11--15",

booktitle = "Proc Eur Conf Des Autom",

note = "Proceedings the European Conference on Design Automation ; Conference date: 16-03-1992 Through 19-03-1992",

}

TY - GEN

T1 - Resolution-based correctness proofs of synchronous circuits

AU - Camurati, Paolo

AU - Margaria, Tiziana

AU - Prinetto, Paolo

PY - 1992

Y1 - 1992

N2 - First-Order theorem provers like OTTER satisfy the vital need for versatility and efficiency in formal verification of correctness. This paper deals with experiences in applying OTTER to synchronous circuits. Synchronous circuits are first modeled, then proved correct by means of demodulation- and hyperresolution-based methodologies. Experimental examples are discussed, results are reported and a first comparison is drawn with other proof styles.

AB - First-Order theorem provers like OTTER satisfy the vital need for versatility and efficiency in formal verification of correctness. This paper deals with experiences in applying OTTER to synchronous circuits. Synchronous circuits are first modeled, then proved correct by means of demodulation- and hyperresolution-based methodologies. Experimental examples are discussed, results are reported and a first comparison is drawn with other proof styles.

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

M3 - Conference contribution

AN - SCOPUS:0027091642

SN - 0818626453

T3 - Proc Eur Conf Des Autom

SP - 11

EP - 15

BT - Proc Eur Conf Des Autom

PB - Publ by IEEE

T2 - Proceedings the European Conference on Design Automation

Y2 - 16 March 1992 through 19 March 1992

ER -

Resolution-based correctness proofs of synchronous circuits

Abstract

Publication series

Conference

Other files and links

Fingerprint

Cite this