A sound and complete shared-variable concurrency model for multi-threaded Java']Java programs

被引：0
|
作者：
de Boer, F. S. [1 ]
机构：
[1] CWI, NL-1009 AB Amsterdam, Netherlands
来源：
Formal Methods for Open Object-Based Distributed Systems, Proceedings | 2007年 / 4468卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper we discuss an assertional proof method for multi-threaded Java programs. The method extends the proof theory for sequential Java programs with a generalization of the Owicki/Gries interference freedom test to threads in Java.
引用
收藏
页码：252 / 268
页数：17
相关论文
共 44 条
  • [41] Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization
    Inverso, Omar
    Tomasco, Ermenegildo
    Fischer, Bernd
    La Torre, Salvatore
    Parlato, Gennaro
    COMPUTER AIDED VERIFICATION, CAV 2014, 2014, 8559 : 585 - 602
  • [42] Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation
    Nazarpour, Hosein
    Falcone, Ylies
    Bensalem, Saddek
    Bozga, Marius
    FORMAL ASPECTS OF COMPUTING, 2017, 29 (06) : 951 - 986
  • [43] Design-time data-access analysis for parallel Java']Java programs with shared-memory communication model
    Stahl, R
    Catthoor, F
    Lauwereins, R
    Verkest, D
    EURO-PAR 2004 PARALLEL PROCESSING, PROCEEDINGS, 2004, 3149 : 206 - 213
  • [44] Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-Threaded C-Programs
    Inverso, Omar
    Nguyen, Truc L.
    Fischer, Bernd
    La Torre, Salvatore
    Parlato, Gennaro
    2015 30TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2015, : 807 - 812
12345