Conference icon

Conference

Relational STE and theorem proving for formal verification of industrial circuit designs

Abstract:

Model checking by symbolic trajectory evaluation, orchestrated in a flexible functional-programming framework, is a well-established technology for correctness verification of industrial-scale circuit designs. Most verifications in this domain require decomposition into subproblems that symbolic trajectory evaluation can handle, and deductive theorem proving has long been proposed as a complement to symbolic trajectory evaluation to enable such compositional reasoning. This paper describes an...

Expand abstract

Actions


Authors


O'Leary, J More by this author
Kaivola, R More by this author
Pages:
97-104
Publication date:
2013
URN:
uuid:fa9c8e48-118a-4fc8-b0b4-2fddbb3e4b01
Source identifiers:
434477
Local pid:
pubs:434477
ISBN:
9780983567837

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP