Verification of Concurrent Programs Using Petri Net Unfoldings

被引：6
|
作者：
Dietsch, Daniel [1 ]
Heizmann, Matthias [1 ]
Klumpp, Dominik [1 ]
Naouar, Mehdi [1 ]
Podelski, Andreas [1 ]
Schaetzle, Claus [1 ]
机构：
[1] Univ Freiburg, Freiburg, Germany
来源：
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2021 | 2021年 / 12597卷
关键词：
Petri nets; Unfoldings; Concurrency; Verification;
D O I：
10.1007/978-3-030-67067-2_9
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Given a verification problem for a concurrent program (with a fixed number of threads) over infinite data domains, we can construct a model checking problem for an abstraction of the concurrent program through a Petri net (a problem which can be solved using McMillan's unfoldings technique). We present a method of abstraction refinement which translates Floyd/Hoare-style proofs for sample traces into additional synchronization constraints for the Petri net.
引用
收藏
页码：174 / 195
页数：22
相关论文
共 50 条
  • [1] Diagnosability verification with Petri net unfoldings
    Madalinski, Agnes
    Nouioua, Farid
    Dague, Philippe
    INTERNATIONAL JOURNAL OF KNOWLEDGE-BASED AND INTELLIGENT ENGINEERING SYSTEMS, 2010, 14 (02) : 49 - 55
  • [2] Verification of Concurrent Assembly Programs with a Petri Net Based Safety Policy
    王生原
    梁英毅
    董渊
    TsinghuaScienceandTechnology, 2007, (06) : 684 - 690
  • [3] Verification of Concurrent Assembly Programs with a Petri Net Based Safety Policy
    Wang, Shengyuan
    Liang, Yingyi
    Dong, Yuan
    Tsinghua Science and Technology, 2007, 12 (06) : 684 - 690
  • [4] Reversibility verification of Petri nets using unfoldings
    Miyamoto, T
    Kumagai, S
    SMC '97 CONFERENCE PROCEEDINGS - 1997 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5: CONFERENCE THEME: COMPUTATIONAL CYBERNETICS AND SIMULATION, 1997, : 4274 - 4278
  • [5] BRANCH TESTING OF CONCURRENT PROGRAMS USING PETRI NET MODELS
    HO, HF
    CHEN, GH
    KUO, TS
    COMPUTING SYSTEMS, 1990, 5 (02): : 116 - 125
  • [6] Branch testing of concurrent programs using Petri net models
    Ho, Hong-Fa
    Chen, Gen-Heuy
    Kuo, Te-Son
    Computer Systems Science and Engineering, 1990, 5 (02): : 116 - 125
  • [7] Characterization of Reachable Attractors Using Petri Net Unfoldings
    Chatain, Thomas
    Haar, Stefan
    Jezequel, Loig
    Pauleve, Loic
    Schwoon, Stefan
    COMPUTATIONAL METHODS IN SYSTEMS BIOLOGY, CMSB 2014, 2014, 8859 : 129 - 142
  • [8] PETRI NET MODELS OF CONCURRENT ADA PROGRAMS
    STANSIFER, R
    MARINESCU, D
    MICROELECTRONICS AND RELIABILITY, 1991, 31 (04): : 577 - 594
  • [9] Canonical prefixes of Petri net unfoldings
    Victor Khomenko
    Maciej Koutny
    Walter Vogler
    Acta Informatica, 2003, 40 : 95 - 118
  • [10] Canonical prefixes of Petri net unfoldings
    Khomenko, V
    Koutny, M
    Vogler, W
    ACTA INFORMATICA, 2003, 40 (02) : 95 - 118
12345