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 条
  • [1] Model Checking in Parallel Logic Controllers Design and Verification
    Doligalski, Michal
    Tkacz, Jacek
    Gratkowski, Tomasz
    PROCEEDINGS OF THE 2015 FEDERATED CONFERENCE ON SOFTWARE DEVELOPMENT AND OBJECT TECHNOLOGIES, 2017, 511 : 35 - 53
  • [2] Parallel Statistical Model Checking for Safety Verification in Smart Grids
    Mancini, Toni
    Mari, Federico
    Melatti, Igor
    Salvo, Ivano
    Tronci, Enrico
    Gruber, Jorn Klaas
    Hayes, Barry
    Prodanovic, Milan
    Elmegaard, Lars
    2018 IEEE INTERNATIONAL CONFERENCE ON COMMUNICATIONS, CONTROL, AND COMPUTING TECHNOLOGIES FOR SMART GRIDS (SMARTGRIDCOMM), 2018,
  • [3] A robust scheduling strategy for moldable scheduling of parallel jobs
    Srinivasan, S
    Krishnamoorthy, S
    Sadayappan, P
    IEEE INTERNATIONAL CONFERENCE ON CLUSTER COMPUTING, PROCEEDINGS, 2003, : 92 - 99
  • [4] READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking
    Wenzel, Makarius
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (118): : 57 - 71
  • [5] Speeding up the Proof Strategy in Formal Software Verification
    Wagner, Markus
    PROCEEDINGS OF THE 2016 GENETIC AND EVOLUTIONARY COMPUTATION CONFERENCE (GECCO'16 COMPANION), 2016, : 1137 - 1138
  • [6] Parallel Stimulus Generation Based on Model Checking for Coherence Protocol Verification
    Zhao, Kang
    Shen, Wenbo
    IEEE TRANSACTIONS ON VERY LARGE SCALE INTEGRATION (VLSI) SYSTEMS, 2015, 23 (12) : 3124 - 3128
  • [7] An equivalence-checking method for scheduling verification in high-level synthesis
    Karfa, Chandan
    Sarkar, Dipankar
    Mandal, Chittaranjan
    Kumar, Pramod
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2008, 27 (03) : 556 - 569
  • [8] Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems
    Ndukwu, Ukachukwu
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2009, (13): : 27 - 39
  • [9] Symbolic simulation as a simplifying strategy for SoC verification with symbolic model checking
    Dumitrescu, E
    Borrione, D
    3RD IEEE INTERNATIONAL WORKSHOP ON SYSTEM-ON-CHIP FOR REAL-TIME APPLICATIONS, PROCEEDINGS, 2003, : 378 - 383
  • [10] An integration of model checking with automated proof checking
    Rajan, S
    Shankar, N
    Srivas, MK
    COMPUTER AIDED VERIFICATION, 1995, 939 : 84 - 97
12345