Verifying properties of hardware and software by predicate abstraction and model checking

被引：0

作者：

Bryant, RE ^{[1
]}

Rajamani, SK ^{[1
]}

机构：

[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA

来源：

ICCAD-2004: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, IEEE/ACM DIGEST OF TECHNICAL PAPERS | 2004年

关键词：

formal verification; predicate abstraction; model checking; symbolic execution; decision procedures;

D O I：

10.1109/ICCAD.2004.1382615

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

This tutorial describes automatic techniques for formally verifying hardware and software by creating Boolean abstractions of the underlying unbounded system state variables.

引用

页码：437 / 438

页数：2

共 50 条

[31] A counter abstraction technique for verifying properties of probabilistic swarm systems [J].

Lomuscio, Alessio ;

Pirovano, Edoardo .

ARTIFICIAL INTELLIGENCE, 2022, 305

[32] Applying Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems [J].

Trindade, Alessandro ;

Ismail, Hussama ;

Cordeiro, Lucas .

2015 BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEMS ENGINEERING (SBESC), 2015, :102-105

[33] Multi-core model checking and maximum satisfiability applied to hardware-software partitioning [J].

Trindade A.B. ;

De FariaDegelo R. ;

Dos Santos E.G., Jr. ;

Ismail H.I. ;

Da Silva H.C. ;

Cordeiro L.C. .

International Journal of Embedded Systems, 2017, 9 (06) :570-582

[34] Model checking: Software and beyond [J].

Clarke, Edmund M. ;

Lerda, Flavio .

JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2007, 13 (05) :639-649

[35] Verifying Temporal Properties of C Programs via Lazy Abstraction [J].

Duan, Zhao ;

Tian, Cong ;

Duan, Zhenhua .

FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2017, 2017, 10610 :122-139

[36] Model checking performability properties [J].

Haverkort, B ;

Cloth, L ;

Hermanns, H ;

Katoen, JP ;

Baier, C .

INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS, PROCEEDINGS, 2002, :103-112

[37] Abstraction for model checking multi-agent systems [J].

Zhou, Conghua ;

Sun, Bo ;

Liu, Zhifeng .

FRONTIERS OF COMPUTER SCIENCE IN CHINA, 2011, 5 (01) :14-25

[38] Abstract BDDs: A technique for using abstraction in model checking [J].

Clarke, E ;

Jha, S ;

Lu, Y ;

Wang, D .

CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 :172-186

[39] Model Checking Complete Requirements Specifications Using Abstraction [J].

Bharadwaj R. ;

Heitmeyer C.L. .

Automated Software Engineering, 1999, 6 (1) :37-68

[40] Abstraction and Model Checking of Core Erlang Programs in Maude [J].

Neuhaeusser, Martin ;

Noll, Thomas .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 176 (04) :147-163

← 1 2 3 4 5 →