Combining theorem proving and trajectory evaluation in an industrial environment

被引：0

作者：

Aagaard, MD ^{[1
]}

Jones, RB ^{[1
]}

Seger, CJH ^{[1
]}

机构：

[1] Intel Corp, Strateg CAD Labs, Hillsboro, OR 97124 USA

来源：

1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS | 1998年

关键词：

D O I：

暂无

中图分类号：

T [工业技术];

学科分类号：

08 ;

摘要：

We describe the verification of the IM: a large, complex (12,000 gates and 1100 latches) circuit that detects and marks the boundaries between Intel architecture (IA-32) instructions. We verified a gate-level model of the IM against an implementation-independent specification of IA-32 instruction lengths. We used theorem proving to to derive 56 model-checking runs and to verify that the model-checking runs imply that the IM meets the specification for all possible sequences of IA-32 instructions. Our verification discovered eight previously unknown bugs.

引用

页码：538 / 541

页数：4

共 50 条

[11] Combining Induction and Saturation-Based Theorem Proving [J].

Echenim, M. ;

Peltier, N. .

JOURNAL OF AUTOMATED REASONING, 2020, 64 (02) :253-294

[12] Analytics - An experiment in combining theorem proving and symbolic computation [J].

Bauer, A ;

Clarke, E ;

Zhao, XD .

JOURNAL OF AUTOMATED REASONING, 1998, 21 (03) :295-325

[13] A dynamic geometry environment for learning theorem proving [J].

Wong, WK ;

Chan, BY ;

Yin, SK .

5th IEEE International Conference on Advanced Learning Technologies, Proceedings, 2005, :15-17

[14] Combining theorem proving with model checking through predicate abstraction [J].

Ray, Sandip ;

Sumners, Rob .

IEEE DESIGN & TEST OF COMPUTERS, 2007, 24 (02) :132-139

[15] Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications [J].

Rusu, Vlad .

TEST AND PROOFS, PROCEEDINGS, 2010, 6143 :135-150

[16] On combining automated theorem proving and digital engineering for general intelligence [J].

Cody, Tyler ;

Beling, Peter A. .

DISRUPTIVE TECHNOLOGIES IN INFORMATION SCIENCES VII, 2023, 12542

[17] Combining finite model generation with theorem proving - Problems and prospects [J].

Slaney, J ;

Surendonk, T .

FRONTIERS OF COMBINING SYSTEMS, 1996, 3 :141-155

[18] Ω-ANTS -: An open approach at combining interactive and automated theorem proving [J].

Benzmüller, C ;

Sorge, V .

SYMBOLIC COMPUTATION AND AUTOMATED REASONING, 2001, :81-97

[19] THEOREM-PROVING AS AN INDUSTRIAL TOOL FOR SYSTEM LEVEL DESIGN [J].

BAINBRIDGE, S ;

CAMILLERI, A ;

FLEMING, R .

IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY, 1992, 10 :253-274

[20] Feasibility Analysis of the EFSM Transition Path Combining Slicing with Theorem Proving [J].

Lu, Gongzheng ;

Miao, Huaikou .

2013 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2013, :153-156

← 1 2 3 4 5 →