Name
Abstract | ||
|---|---|---|
We report on the design and formal verification of a complex processor supporting address translation by means of a memory management unit (MMU). We give a paper and pencil proof that such a processor together with an appropriate page fault handler simulates virtual machines modeling user computation. These results are crucial steps towards the seamless verification of entire computer systems. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11560548_23 | CHARME |
Keywords | Field | DocType |
pencil proof,user computation,crucial step,memory management unit,seamless verification,appropriate page fault handler,entire computer system,address translation,memory management mechanism,complex processor,formal verification,memory management,virtual machine | Functional verification,Virtual machine,Computer science,Virtual memory,Page table,Memory management,Page fault,Memory management unit,Embedded system,Formal verification | Conference |
Volume | ISSN | ISBN |
3725 | 0302-9743 | 3-540-29105-9 |
Citations | PageRank | References |
23 | 1.81 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Iakov Dalinger | 1 | 23 | 1.81 |
| Mark Hillebrand | 2 | 365 | 16.45 |
| Wolfgang J. Paul | 3 | 89 | 7.54 |