Conference item icon

Conference item

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


Host title:
2013 Formal Methods in Computer-Aided Design, FMCAD 2013
Pages:
97-104
Publication date:
2013-01-01
ISBN:
9780983567837
Pubs id:
pubs:434477
UUID:
uuid:fa9c8e48-118a-4fc8-b0b4-2fddbb3e4b01
Local pid:
pubs:434477
Source identifiers:
434477
Deposit date:
2014-02-28

Terms of use


Views and Downloads






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

TO TOP