Name
Abstract | ||
|---|---|---|
Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/s11390-020-0536-9 | JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY |
Keywords | Field | DocType |
Scalable Processor Architecture Version 8 (SPARCv8), assembly code verification, context switch, Coq, refinement verification | System software,Embedded operating system,Programming language,Computer science,Correctness,Inline assembler,Assembly language,Register window,Modular design,Context switch | Conference |
Volume | Issue | ISSN |
35 | 6 | 1000-9000 |
Citations | PageRank | References |
0 | 0.34 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Junpeng Zha | 1 | 0 | 0.34 |
| Xinyu Feng | 2 | 443 | 30.52 |
| Lei Qiao | 3 | 2 | 5.43 |