Model Check of Real-time Property of Embedded Assembly Program Using CEGAR

被引：1

作者：

Kamide, Hiromu ^{[1
]}

Uemura, Kosuke ^{[1
]}

Yamane, Satoshi ^{[1
]}

机构：

[1] Kanazawa Univ, Inst Sci & Engn, Kakuma Machi, Kanazawa, Ishikawa 9201192, Japan

来源：

2018 IEEE 42ND ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1 | 2018年

关键词：

Formal Verification; Model Checking; Assembler Language; CEGAR; Lazy Abstraction; Refinement;

D O I：

10.1109/COMPSAC.2018.00126

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

In program verification research, the methods using abstraction have been actively conducted recently. In this research, we propose a method for verifying real-time property by applying abstraction and refinement technique to embedded assembly program.

引用

页码：799 / 800

页数：2