Generalization, lemma generation, and induction in ACL2
Formal verification is becoming a critical tool for designing software and hardware today. Rising complexity, along with software's pervasiveness in the global economy have meant that errors are becoming more difficult to find and more costly to fix. Among the formal verification tools availabl...
| Main Author: | |
|---|---|
| Format: | Others |
| Language: | English |
| Published: |
2008
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/2152/4004 |