Automatic verification of a model checker by reflection

被引：0

作者：

Wang, BY ^{[1
]}

机构：

[1] Acad Sinica, Inst Informat Sci, Taipei 115, Taiwan

来源：

PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES | 2006年 / 3819卷

关键词：

reflection; rewriting logic; model checking; logic programming;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Intuitively, reflection is the feature that can represent and reason meta-level entities at the object level. In this paper, we use a reflective language to implement a local model checker and analyze the implementation. The implementation is greatly simplified by reflection. Further, we show the feature can be applied to verify the concise implementation rather easily. The simplicity of our approach suggests that reflection may be useful in the implementation and verification of other explicit-state model checking algorithms.

引用

页码：45 / 59

页数：15

共 50 条

[11] SURVEY ON PARAMETERIZED VERIFICATION WITH THRESHOLD AUTOMATA AND THE BYZANTINE MODEL CHECKER
Konnov, Igor
Lazic, Marijana
Stoilkovska, Ilina
Widder, Josef
LOGICAL METHODS IN COMPUTER SCIENCE, 2023, 19 (01) : 1 - 5
[12] Using CTL Model Checker for Verification of Domain Application Systems
Cacovean, Laura Florentina
RECENT ADVANCES IN NEURAL NETWORKS, FUZZY SYSTEMS & EVOLUTIONARY COMPUTING, 2010, : 262 - 267
[13] SMC: A symmetry based model checker for verification of liveness properties
Sistla, AP
Miliades, L
Gyuris, V
COMPUTER AIDED VERIFICATION, 1997, 1254 : 464 - 467
[14] Modeling and verification of marine equipment systems using a model checker
Yao, Shunsuke
Awano, Hiroaki
Hiraoka, Yasushi
Takahashi, Kazuko
IMECS 2008: INTERNATIONAL MULTICONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, VOLS I AND II, 2008, : 1033 - +
[15] NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification
Yuan, Yifei
Moon, Soo-Jin
Uppal, Sahil
Jia, Limin
Sekar, Vyas
PROCEEDINGS OF THE 17TH USENIX SYMPOSIUM ON NETWORKED SYSTEMS DESIGN AND IMPLEMENTATION, 2020, : 181 - 200
[16] Verification of Behavioral Domain-Specific Languages with a Model Checker
Ammann, Christian
MECHANICAL ENGINEERING AND TECHNOLOGY, 2012, 125 : 779 - 782
[17] AUTOMATIC DISOMETER CHECKER
WALSH, ML
NUCLEAR INSTRUMENTS & METHODS, 1971, 97 (02): : 425 - &
[18] Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
Brunner, Julian
Lammich, Peter
JOURNAL OF AUTOMATED REASONING, 2018, 60 (01) : 3 - 21
[19] A Lightweight Integration of Mutation Analysis with the Model Checker for System Safety Verification
Jayanthi, J.
Nanda, Manju
Nayak, Sameer
2013 7TH ANNUAL IEEE INTERNATIONAL SYSTEMS CONFERENCE (SYSCON 2013), 2013, : 76 - 81
[20] Concurrent Usage Control Implementation Verification Using the SPIN Model Checker
Rajkumar, P. V.
Ghosh, S. K.
Dasgupta, P.
RECENT TRENDS IN NETWORK SECURITY AND APPLICATIONS, 2010, 89 : 214 - +

← 1 2 3 4 5 →