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 条
  • [1] Relational interprocedural verification of concurrent programs
    Bertrand Jeannet
    Software & Systems Modeling, 2013, 12 : 285 - 306
  • [2] Relational interprocedural verification of concurrent programs
    Jeannet, Bertrand
    SOFTWARE AND SYSTEMS MODELING, 2013, 12 (02): : 285 - 306
  • [3] Mechanized Relational Verification of Concurrent Programs with Continuations
    Timany, Amin
    Birkedal, Lars
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (ICFP):
  • [4] Precise slicing of interprocedural concurrent programs
    Qi, Xiaofang
    Jiang, Zhenliang
    FRONTIERS OF COMPUTER SCIENCE, 2017, 11 (06) : 971 - 986
  • [5] Precise slicing of interprocedural concurrent programs
    Xiaofang Qi
    Zhenliang Jiang
    Frontiers of Computer Science, 2017, 11 : 971 - 986
  • [6] Frameworks for Interprocedural Analysis of Concurrent Programs
    Seidl, Helmut
    Apinis, Kalmer
    Vojdani, Vesal
    SOFTWARE SYSTEMS SAFETY, 2014, 36 : 309 - 347
  • [7] Interprocedural analysis of concurrent programs under a context bound
    Lal, Akash
    Touili, Tayssir
    Kidd, Nicholas
    Reps, Thomas
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 282 - +
  • [8] CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs
    Liu, Peizun
    Wahl, Thomas
    ACM SIGPLAN NOTICES, 2018, 53 (04) : 105 - 119
  • [9] CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs
    Liu, Peizun
    Wahl, Thomas
    PROCEEDINGS OF THE 39TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, PLDI 2018, 2018, : 105 - 119
  • [10] Abstracting call-stacks for interprocedural verification of imperative programs
    Jeannet, B
    Serwe, W
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 258 - 273
12345