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 条
  • [1] A formal transformation and refinement method for concurrent programs
    Younger, EJ
    Bennett, KH
    Luo, Z
    [J]. INTERNATIONAL CONFERENCE ON SOFTWARE MAINTENANCE, PROCEEDINGS, 1997, : 287 - 294
  • [2] Automated and Modular Refinement Reasoning for Concurrent Programs
    Hawblitzel, Chris
    Petrank, Erez
    Qadeer, Shaz
    Tasiran, Serdar
    [J]. COMPUTER AIDED VERIFICATION, CAV 2015, PT II, 2015, 9207 : 449 - 465
  • [3] STRUCTURED PARTITIONING OF CONCURRENT PROGRAMS FOR EXECUTION ON MULTIPROCESSORS
    WANG, CM
    WANG, SD
    [J]. PARALLEL COMPUTING, 1990, 16 (01) : 41 - 57
  • [4] A structured approach to develop concurrent programs in UML
    Mizuno, M
    Singh, G
    Neilsen, M
    [J]. UML 2000 - THE UNIFIED MODELING LANGUAGE, PROCEEDINGS: ADVANCING THE STANDARD, 2000, 1939 : 451 - 465
  • [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] A structured approach for developing concurrent programs in Java']Java
    Mizuno, M
    [J]. INFORMATION PROCESSING LETTERS, 1999, 69 (05) : 233 - 238
  • [7] Towards a refinement calculus for concurrent real-time programs
    Peuker, S
    Hayes, I
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2495 : 335 - 346
  • [8] Counterexample-guided abstraction refinement for symmetric concurrent programs
    Alastair F. Donaldson
    Alexander Kaiser
    Daniel Kroening
    Michael Tautschnig
    Thomas Wahl
    [J]. Formal Methods in System Design, 2012, 41 : 25 - 44
  • [9] Non-monotonic Refinement of Control Abstraction for Concurrent Programs
    Gupta, Ashutosh
    Popeea, Corneliu
    Rybalchenko, Andrey
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2010, 6252 : 188 - 202
  • [10] Counterexample-guided abstraction refinement for symmetric concurrent programs
    Donaldson, Alastair F.
    Kaiser, Alexander
    Kroening, Daniel
    Tautschnig, Michael
    Wahl, Thomas
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2012, 41 (01) : 25 - 44
12345