Refinement for Structured Concurrent Programs

被引：4
|
作者：
Kragl, Bernhard [1 ]
Qadeer, Shaz [2 ]
Henzinger, Thomas A. [1 ]
机构：
[1] IST Austria, Klosterneuburg, Austria
[2] Novi, Seattle, WA USA
来源：
COMPUTER AIDED VERIFICATION (CAV 2020), PT I | 2020年 / 12224卷
基金：
奥地利科学基金会;
关键词：
D O I：
10.1007/978-3-030-53288-8_14
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper presents a foundation for refining concurrent programs with structured control flow. The verification problem is decomposed into subproblems that aid interactive program development, proof reuse, and automation. The formalization in this paper is the basis of a new design and implementation of the CIVL verifier.
引用
收藏
页码：275 / 298
页数：24
相关论文
共 50 条
  • [41] Relational Concurrent Refinement with Internal Operations
    Derrick, John
    Boiten, Eerke
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 187 : 35 - 53
  • [42] Modelling Divergence in Relational Concurrent Refinement
    Boitlen, Eerke
    Derrick, John
    [J]. INTEGRATED FORMAL METHODS, PROCEEDINGS, 2009, 5423 : 183 - +
  • [43] Tractable Refinement Checking for Concurrent Objects
    Bouajjani, Ahmed
    Emmi, Michael
    Enea, Constantin
    Hamza, Jad
    [J]. ACM SIGPLAN NOTICES, 2015, 50 (01) : 651 - 662
  • [44] Refinement algebra for probabilistic programs
    Meinicke, Larissa
    Solin, Kim
    [J]. FORMAL ASPECTS OF COMPUTING, 2010, 22 (01) : 3 - 31
  • [45] Automating Refinement of Circus Programs
    Zeyda, Frank
    Cavalcanti, Ana
    [J]. FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, 2011, 6527 : 274 - 290
  • [46] A refinement calculus for logic programs
    Hayes, I
    Colvin, R
    Hemer, D
    Strooper, P
    Nickson, R
    [J]. THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2002, 2 : 425 - 460
  • [47] Structured Communications with Concurrent Constraints
    Coppo, Mario
    Dezani-Ciancaglini, Mariangiola
    [J]. TRUSTWORTHY GLOBAL COMPUTING, 2009, 5474 : 104 - 125
  • [48] STRUCTURED REPORT PROGRAMS
    MATLAK, EW
    [J]. JOURNAL OF SYSTEMS MANAGEMENT, 1978, 29 (10): : 42 - 45
  • [49] ANALYSIS OF STRUCTURED PROGRAMS
    KOSARAJU, SR
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1974, 9 (03) : 232 - 255
  • [50] An approach to local refinement of structured grids
    Durbin, PA
    Iaccarino, G
    [J]. JOURNAL OF COMPUTATIONAL PHYSICS, 2002, 181 (02) : 639 - 653
12345