Modular Verification of SPARCv8 Code

被引：1

作者：

Zha, Junpeng ^{[1
]}

Feng, Xinyu ^{[2
]}

Qiao, Lei ^{[3
]}

机构：

[1] Univ Sci & Technol China, Hefei, Peoples R China

[2] Nanjing Univ, State Key Lab Novel Software Technol, Nanjing, Peoples R China

[3] Beijing Inst Control Engn, Beijing, Peoples R China

来源：

PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2018 | 2018年 / 11275卷

基金：

中国国家自然科学基金;

关键词：

LOGIC;

D O I：

10.1007/978-3-030-02768-1_14

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Inline assembly code is common in system software to interact with the underlying hardware platforms. 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 assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA, including delayed control transfers, delayed writes to special registers, and register windows. We have applied it to verify the main body of a context switch routine in a realistic embedded OS kernel. All of the formalization and proofs have been mechanized in Coq.

引用

页码：245 / 263

页数：19

共 50 条

[21] Modular Indirect Push-Button Formal Verification of Multi-threaded Code Generators
Wijs, Anton
Wilkowski, Maciej
SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2019), 2019, 11724 : 410 - 429
[22] Automating modular verification
Alur, R
de Alfaro, L
Henzinger, TA
Mang, FYC
CONCUR '99: CONCURRENCY THEORY, 1999, 1664 : 82 - 97
[23] Modular verification of multipliers
Ravi, K
Pardo, A
Hachtel, GD
Somenzi, F
FORMAL METHODS IN COMPUTER-AIDED DESIGN, 1996, 1166 : 49 - 63
[24] Code Verification for the SENSEI CFD Code
Xue, Weicheng
Wang, Hongyu
Roy, Christopher J.
JOURNAL OF VERIFICATION, VALIDATION AND UNCERTAINTY QUANTIFICATION, 2023, 8 (02):
[25] Modular verification of modular finite state machines
Endsley, EW
Tilbury, DM
2004 43RD IEEE CONFERENCE ON DECISION AND CONTROL (CDC), VOLS 1-5, 2004, : 972 - 979
[26] Verification conditions are code
Gravell, Andrew M.
ACTA INFORMATICA, 2007, 43 (06) : 431 - 447
[27] Verification conditions are code
Andrew M. Gravell
Acta Informatica, 2007, 43 : 431 - 447
[28] Shutdown dose rate analysis with the Shift Monte Carlo radiation transport code and modular verification workflow
Bae, Jin Whan
Kos, Bor
Biondo, Elliott
FUSION ENGINEERING AND DESIGN, 2023, 194
[29] Verification of the SCALE modular code system for criticality safety and depletion analyses of WWER spent fuel facilities
Apostolov, T
Manolova, M
Belousov, S
Prodanova, R
STORAGE OF SPENT FUEL FROM POWER REACTORS, 2003, 20 : 348 - 359
[30] Code Mutation in Verification and Automatic Code Correction
Katz, Gal
Peled, Doron
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2010, 6015 : 435 - 450

← 1 2 3 4 5 →