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...
Автори: | O'Leary, J, Kaivola, R, Melham, T |
---|---|
Формат: | Conference item |
Опубліковано: |
2013
|
Схожі ресурси
Схожі ресурси
-
Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs
за авторством: O'Leary, J, та інші
Опубліковано: (2013) -
A Reflective Functional Language for Hardware Design and Theorem Proving
за авторством: Grundy, J, та інші
Опубліковано: (2006) -
A Reflective Functional Language for Hardware Design and Theorem Proving
за авторством: Grundy, J, та інші
Опубліковано: (2003) -
Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving
за авторством: Aagaard, M, та інші
Опубліковано: (1999) -
Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version)
за авторством: Aagaard, M, та інші
Опубліковано: (2000)