Relational interprocedural verification of concurrent programs

被引：6
|
作者：
Jeannet, Bertrand [1 ]
机构：
[1] INRIA Grenoble Rhone Alpes, Grenoble, France
来源：
SEFM 2009: SEVENTH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS | 2009年
关键词：
D O I：
10.1109/SEFM.2009.29
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We propose a general analysis method for recursive, concurrent programs that tracks effectively procedure calls and returns in a concurrent context, even in the presence of unbounded recursion and infinite-state variables like integers. This method generalizes the relational interprocedural analysis of sequential programs to the concurrent case. We implemented it for programs with scalar variables, and we experimented several classical synchronisation protocols in order to illustrate the precision of our technique, but also to analyze the approximations it performs.
引用
收藏
页码：83 / 92
页数：10
相关论文
共 50 条
  • [21] Verification of Fine-grain Concurrent Programs
    Hoare, Tony
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 209 : 165 - 171
  • [22] Automatic verification of timed concurrent constraint programs
    Falaschi, Moreno
    Villanueva, Alicia
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2006, 6 : 265 - 300
  • [23] FORMAL VERIFICATION OF A CLASS OF CONCURRENT PROGRAMS.
    Mori, Masaaki
    Taniguchi, Kenichi
    Kasami, Tadao
    Fujii, Mamoru
    Systems, computers, controls, 1981, 10 (04): : 11 - 20
  • [24] COMPLX: A Verification Framework for Concurrent Imperative Programs
    Amani, Sidney
    Andronick, June
    Bortin, Maksym
    Lewis, Corey
    Rizkallah, Christine
    Tuong, Joseph
    PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17, 2017, : 138 - 150
  • [25] Verification of Concurrent Programs on Weak Memory Models
    Travkin, Oleg
    Wehrheim, Heike
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2016, 2016, 9965 : 3 - 24
  • [26] Efficient Verification of Sequential and Concurrent C Programs
    S. Chaki
    E. Clarke
    A. Groce
    J. Ouaknine
    O. Strichman
    K. Yorav
    Formal Methods in System Design, 2004, 25 : 129 - 166
  • [27] Specification and Verification of Concurrent Programs Through Refinements
    Sandip Ray
    Rob Sumners
    Journal of Automated Reasoning, 2013, 51 : 241 - 280
  • [28] A dynamic logic for deductive verification of concurrent programs
    Beckert, Bernhard
    Klebanov, Vladimir
    SEFM 2007: FIFTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2007, : 141 - +
  • [29] PBMC: Symbolic Slicing for the Verification of Concurrent Programs
    Saissi, Habib
    Bokor, Peter
    Suri, Neeraj
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 : 344 - 360
  • [30] Verification of Concurrent Programs: Decidability, Complexity, Reductions
    Bouajjani, Ahmed
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2014, 2014, 8837 : XI - XI
12345