A scheduling strategy for parallel proof checking and verification

被引：0

作者：

He Pei ^{[1
]}

Kang Lishan ^{[2
]}

Xiao Zengliang ^{[3
]}

Xiao Zhuoyu ^{[3
]}

机构：

[1] Wuhan Univ, State Key Lab Software Engn, Wuhan 430072, Peoples R China

[2] Wuhan Univ, China Univ Geosci, Wuhan 430072, Peoples R China

[3] Changsha Univ Sci & Technol, Changsha, Hunan 410076, Peoples R China

来源：

PROCEEDINGS OF 2008 IEEE INTERNATIONAL CONFERENCE ON NETWORKING, SENSING AND CONTROL, VOLS 1 AND 2 | 2008年

基金：

中国国家自然科学基金;

关键词：

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Proof checking is one of the major concerns of many mechanized formal approaches. This paper first deals with scheduling issues related to parallel proof checking, then applies the obtained result and similar idea to parallel verifications. To facilitate understanding, the discussion is based on INCAPS, an interactive deduction system of temporal logic. This method can also be adapted for improving other mechanized formal systems.

引用

页码：1823 / +

页数：2

共 50 条

[21] On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
Barnat, Jiri
Brim, Lubos
Rockai, Petr
SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (12) : 1272 - 1288
[22] PVS: Combining specification, proof checking, and model checking
Shankar, N
FORMAL METHODS IN COMPUTER-AIDED DESIGN, 1996, 1166 : 257 - 264
[23] A Proof Theory for Model Checking
Quentin Heath
Dale Miller
Journal of Automated Reasoning, 2019, 63 : 857 - 885
[24] Proof Checking and Knowledge by Intellection
Philosophical Studies, 1998, 92 : 85 - 112
[25] Proof checking and logic programming
Miller, Dale
FORMAL ASPECTS OF COMPUTING, 2017, 29 (03) : 383 - 399
[26] Proof-checking Euclid
Beeson, Michael
Narboux, Julien
Wiedijk, Freek
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2019, 85 (2-4) : 213 - 257
[27] A Proof Theory for Model Checking
Heath, Quentin
Miller, Dale
JOURNAL OF AUTOMATED REASONING, 2019, 63 (04) : 857 - 885
[28] Towards lean proof checking
Barthe, G
Elbers, H
DESIGN AND IMPLEMENTATION OF SYMBOLIC COMPUTATION SYSTEMS, 1996, 1128 : 61 - 62
[29] Proof checking and logic programming
Miller, Dale
PROCEEDINGS OF THE 17TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2015), 2015, : 18 - 18
[30] Proof-checking Euclid
Michael Beeson
Julien Narboux
Freek Wiedijk
Annals of Mathematics and Artificial Intelligence, 2019, 85 : 213 - 257

← 1 2 3 4 5 →