Name
Abstract | ||
|---|---|---|
Symbolic execution has long been a staple technique for formal hardware verification. Its application to software requires methods for dealing with software specific complexities. In this paper we elaborate methods for the efficient symbolic simulation of embedded software; some methods are new, others are improvements of existing methods. Using these techniques we have been able to symbolically execute real life microcode of thousands of lines, allowing formal methods to become an integral part of microcode validation in Intel Corporation. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1145/1403375.1403577 | Proceedings of the conference on Design, automation and test in Europe |
Keywords | Field | DocType |
concrete,application software,formal method,hardware,software requirements,formal verification,embedded software,software specification | Symbolic simulation,Microcode,Embedded software,Programming language,Computer science,Parallel computing,Software,Symbolic execution,Formal methods,Software verification and validation | Conference |
ISSN | Citations | PageRank |
1530-1591 | 8 | 0.57 |
References | Authors | |
9 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tamarah Arons | 1 | 278 | 14.59 |
| Elad Elster | 2 | 32 | 1.87 |
| Shlomit Ozer | 3 | 8 | 0.57 |
| Jonathan Shalev | 4 | 56 | 10.75 |
| Eli Singerman | 5 | 283 | 20.61 |