Loading...
Please wait, while we are loading the content...
Similar Documents
Formal proof of the avm-1 microprocessor using the concept of generic interpreters
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Cohen, G. C. Windley, P. Levitt, K. |
| Copyright Year | 1991 |
| Description | A microprocessor designated AVM-1 was designed to demonstrate the use of generic interpreters in verifying hierarchically decomposed microprocessor specifications. This report is intended to document the high-order language (HOL) code verifying AVM-1. The organization of the proof is discussed and some technical details concerning the execution of the proof scripts in HOL are presented. The proof scripts used to verify AVM-1 are also presented. |
| File Size | 4970704 |
| Page Count | 216 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_19910010443 |
| Archival Resource Key | ark:/13960/t3tt9j07r |
| Language | English |
| Publisher Date | 1991-03-01 |
| Access Restriction | Open |
| Subject Keyword | Hierarchies Architecture Computers Microprocessors High Level Languages Computer Programs Proving Ntrs Nasa Technical Reports ServerĀ (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |