Name
Abstract | ||
|---|---|---|
Microcode is used to facilitate new technologies in Intel CPU designs. A critical requirement is that new designs be backwardly compatible with legacy code when new functionalities are disabled. Several features distinguish microcode from other software systems, such as: interaction with the external environment, sensitivity to exceptions, and the complexity of instructions. This work describes the ideas behind MICROFORMAL,, a technology for fully automated formal verification of functional backward compatibility of microcode. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11513988_20 | CAV |
Keywords | Field | DocType |
software system,critical requirement,new technology,legacy code,external environment,intel cpu design,new functionalities,formal verification,new design,software systems | Microcode,Programming language,Computer science,Algorithm,Software system,Symbolic execution,Legacy code,Software architecture,Backward compatibility,Legacy system,Formal verification | Conference |
Volume | ISSN | ISBN |
3576 | 0302-9743 | 3-540-27231-3 |
Citations | PageRank | References |
24 | 1.29 | 12 |
Authors | ||
10 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tamarah Arons | 1 | 278 | 14.59 |
| Elad Elster | 2 | 32 | 1.87 |
| Limor Fix | 3 | 937 | 118.11 |
| Sela Mador-Haim | 4 | 174 | 6.87 |
| Michael Mishaeli | 5 | 24 | 1.29 |
| Jonathan Shalev | 6 | 56 | 10.75 |
| Eli Singerman | 7 | 283 | 20.61 |
| Andreas Tiemeyer | 8 | 45 | 3.41 |
| Moshe Y. Vardi | 9 | 13413 | 2267.07 |
| Lenore D. Zuck | 10 | 1559 | 141.69 |