The verification of MDG algorithms in the HOL theorem prover
Formal verification of digital systems is achieved, today, using one of two main approaches: states exploration (mainly model checking and equivalence checking) or deductive reasoning (theorem proving). Indeed, the combination of the two approaches, states exploration and deductive reasoning promise...
| Main Author: | |
|---|---|
| Format: | Others |
| Published: |
2008
|
| Online Access: | http://spectrum.library.concordia.ca/976015/1/NR42548.pdf Abed, Sa'ed Rasmi H <http://spectrum.library.concordia.ca/view/creators/Abed=3ASa=27ed_Rasmi_H=3A=3A.html> (2008) The verification of MDG algorithms in the HOL theorem prover. PhD thesis, Concordia University. |