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
相关论文
共 23 条
  • [1] Alglave Jade, 2013, Computer Aided Verification. 25th International Conference, CAV 2013. Proceedings. LNCS 8044, P141, DOI 10.1007/978-3-642-39799-8_9
  • [2] Apt K.R., 2009, Texts in Computer Science
  • [3] Berdine J, 2008, LECT NOTES COMPUT SC, V5123, P399
  • [4] Reliable benchmarking: requirements and solutions
    Beyer, Dirk
    Loewe, Stefan
    Wendler, Philipp
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2019, 21 (01) : 1 - 29
  • [5] Verification of Concurrent Programs Using Trace Abstraction Refinement
    Cassez, Franck
    Ziegler, Frowin
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, (LPAR-20 2015), 2015, 9450 : 233 - 248
  • [6] Donaldson Alastair, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P356, DOI 10.1007/978-3-642-22110-1_28
  • [7] Dräger K, 2010, LECT NOTES COMPUT SC, V6015, P271, DOI 10.1007/978-3-642-12002-2_22
  • [8] A framework to synergize partial order reduction with state interpolation
    [J]. 1600, Springer Verlag (8855): : 171 - 187
  • [9] An improvement of McMillan's unfolding algorithm
    Esparza, J
    Römer, S
    Vogler, W
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2002, 20 (03) : 285 - 310
  • [10] Reductions for Safety Proofs
    Farzan, Azadeh
    Vandikas, Anthony
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
123