Formal verification of design correctness of sequential circuits based on theorem provers

Paolo Camurati, Tiziana Margaria, Paolo Prinetto

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

After a presentation of alternative time modeling techniques, the description techniques available in OTTER, a first-order logic proof environment at the different abstraction levels are presented. A discussion is presented of the methodology envisaged for the proof of correctness and its implementation in OTTER depending on the circuit characteristics and on the reasoning technique. Some experimental results are also reported.

Original languageEnglish
Title of host publicationProceedings, Advanced Computer Technology, Reliable Systems and Applications
PublisherPubl by IEEE
Pages322-326
Number of pages5
ISBN (Print)0818621419
Publication statusPublished - 1991
EventProceedings of the 5th European Computer Conference on Advanced Computer Technology, Reliable Systems and Applications - CompEuro 91 - Bologna, Italy
Duration: 13 May 199116 May 1991

Publication series

NameProceedings, Advanced Computer Technology, Reliable Systems and Applications

Conference

ConferenceProceedings of the 5th European Computer Conference on Advanced Computer Technology, Reliable Systems and Applications - CompEuro 91
CityBologna, Italy
Period13/05/9116/05/91

Fingerprint

Dive into the research topics of 'Formal verification of design correctness of sequential circuits based on theorem provers'. Together they form a unique fingerprint.

Cite this