Relational STE and theorem proving for formal verification of industrial circuit designs
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 tra...
Autores principales: | O'Leary, J, Kaivola, R, Melham, T |
---|---|
Formato: | Conference item |
Publicado: |
2013
|
Ejemplares similares
-
Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs
por: O'Leary, J, et al.
Publicado: (2013) -
A Reflective Functional Language for Hardware Design and Theorem Proving
por: Grundy, J, et al.
Publicado: (2006) -
A Reflective Functional Language for Hardware Design and Theorem Proving
por: Grundy, J, et al.
Publicado: (2003) -
Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving
por: Aagaard, M, et al.
Publicado: (1999) -
Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version)
por: Aagaard, M, et al.
Publicado: (2000)