Hardware Model Checking Algorithms and Techniques

被引：1

作者：

Cabodi, Gianpiero ^{[1
]}

Camurati, Paolo Enrico ^{[1
]}

Palena, Marco ^{[2
]}

Pasini, Paolo ^{[3
]}

机构：

[1] Politecn Torino, DAUIN, Dept Control & Comp Engn, I-10129 Turin, Italy

[2] Natl Interuniv Consortium Telecommun, CNIT, I-10129 Turin, Italy

[3] Politecn Torino, DET, Dept Elect & Telecommun, I-10129 Turin, Italy

来源：

ALGORITHMS | 2024年 / 17卷 / 06期

关键词：

formal verification; model checking; SAT; Boolean functions; LOWER BOUNDS; INTERPOLATION; SYSTEMS;

D O I：

10.3390/a17060253

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Digital systems are nowadays ubiquitous and often comprise an extremely high level of complexity. Guaranteeing the correct behavior of such systems has become an ever more pressing need for manufacturers. The correctness of digital systems can be addressed resorting to formal verification techniques, such as model checking. Currently, it is usually impossible to determine a priori the best algorithm to use given a verification task and, thus, portfolio approaches have become the de facto standard in model checking verification suites. This paper describes the most relevant algorithms and techniques, at the foundations of bit-level SAT-based model checking itself.

引用

页数：55

共 50 条

[21] GRAFCET Reduction Techniques for Model Checking
Mross, Robin
Schnakenbeck, Aron
Voelker, Marcus
Fay, Alexander
Kowalewski, Stefan
2023 IEEE 21ST INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS, INDIN, 2023,
[22] Techniques for temporal logic model checking
Deharbe, David
REFINEMENT TECHNIQUES IN SOFTWARE ENGINEERING, 2006, 3167 : 315 - 367
[23] Implementation Techniques for Mathematical Model Checking
Schreiner, Wolfgang
2022 24TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING, SYNASC, 2022, : 12 - 15
[24] Visualization Techniques for Topic Model Checking
Murdock, Jaimie
Allen, Colin
PROCEEDINGS OF THE TWENTY-NINTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2015, : 4284 - 4285
[25] Integrating temporal logics and model checking algorithms
Rus, T
Van Wyk, E
TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT, 1997, 1231 : 95 - 110
[26] Model checking randomized algorithms with Java PathFinder
DisCoVeri Group, Department of Computer Science and Engineering, York University, Toronto, Canada
Proc. - Int. Conf. Quant. Eval. Syst., QEST, (157-158):
[27] On Model-Checking Optimistic Replication Algorithms
Boucheneb, Hanifa
Imine, Abdessamad
FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2009, 5522 : 73 - +
[28] Model checking for nonmonotonic logics: algorithms and complexity
Rosati, R
IJCAI-99: PROCEEDINGS OF THE SIXTEENTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOLS 1 & 2, 1999, : 76 - 81
[29] Automated Model Design using Genetic Algorithms and Model Checking
Lefticaru, Raluca
Ipate, Florentin
Tudose, Cristina
PROCEEDINGS OF THE 2009 FOURTH BALKAN CONFERENCE IN INFORMATICS, 2009, : 79 - 84
[30] Word level bitwidth reduction for unbounded hardware model checking
Per Bjesse
Formal Methods in System Design, 2009, 35 : 56 - 72

← 1 2 3 4 5 →