Relational interprocedural verification of concurrent programs

被引：12
作者：
Jeannet, Bertrand [1 ]
机构：
[1] INRIA, Grenoble, France
来源：
SOFTWARE AND SYSTEMS MODELING | 2013年 / 12卷 / 02期
关键词：
Concurrent program analysis; Interprocedural analysis; Abstract interpretation; Numerical abstract domains; Forward and backward analysis;
D O I：
10.1007/s10270-012-0230-7
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We propose a general analysis method for recursive, concurrent programs that track effectively procedure calls and return 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, and extends it to backward or coreachability analysis. We implemented it for programs with scalar variables and experimented with several classical synchronization protocols in order to illustrate the precision of our technique and also to analyze the approximations it performs.
引用
收藏
页码：285 / 306
页数：22
相关论文
共 37 条
  • [21] Automatic verification of confidentiality properties of cryptographic programs
    El Kadhi, N
    [J]. 8TH WORLD MULTI-CONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XIII, PROCEEDINGS: INDUSTRIAL SYSTEMS, 2004, : 248 - 256
  • [22] Dataflow analysis for concurrent programs using datarace detection
    Chugh, Ravi
    Voung, Jan W.
    Jhala, Ranjit
    Lerner, Sorin
    [J]. ACM SIGPLAN NOTICES, 2008, 43 (06) : 316 - 326
  • [23] A Framework for Abstract Interpretation of Timed Concurrent Constraint Programs
    Falaschi, Moreno
    Olarte, Carlos
    Palamidessi, Catuscia
    [J]. PPDP'09: PROCEEDINGS OF THE 11TH INTERNATIONAL ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2009, : 207 - 217
  • [24] Dataflow Analysis for Concurrent Programs using Datarace Detection
    Chugh, Ravi
    Voung, Jan W.
    Jhala, Ranjit
    Lerner, Sorin
    [J]. PLDI'08: PROCEEDINGS OF THE 2008 SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN & IMPLEMENTATION, 2008, : 316 - 326
  • [25] A Practical Type Analysis for Verification of Modular Prolog Programs
    Pietrzak, Pawel
    Correas, Jesus
    Puebla, German
    Hermenegildo, Manuel V.
    [J]. PEPM'08: PROCEEDINGS OF THE 2008 ACM SIGPLAN SYMPOSIUM ON PARTIAL EVALUATION AND SEMANTICS-BASED PROGRAM MANIPULATION, 2008, : 61 - 70
  • [26] Verifying Safety Properties of Concurrent Heap-Manipulating Programs
    Yahav, Eran
    Sagiv, Mooly
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2010, 32 (05):
  • [27] Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
    Erhard, Julian
    Bentele, Manuel
    Heizmann, Matthias
    Klumpp, Dominik
    Saan, Simmo
    Schuessele, Frank
    Schwarz, Michael
    Seidl, Helmut
    Tilscher, Sarah
    Vojdani, Vesal
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2025, PT I, 2025, 15529 : 74 - 100
  • [28] Static analysis for concurrent programs with applications to data race detection
    Kahlon V.
    Sankaranarayanan S.
    Gupta A.
    [J]. International Journal on Software Tools for Technology Transfer, 2013, 15 (4) : 321 - 336
  • [29] A Thread Modularity Approach for Verification Concurrent Software Based on Abstract Interpretation
    Jiang, Qingyu
    Liu, Jing
    Hu, Haodong
    [J]. 2018 25TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2018), 2018, : 119 - 128
  • [30] Verification of Erlang programs using abstract interpretation and model checking
    Huch, F
    [J]. ACM SIGPLAN NOTICES, 1999, 34 (09) : 261 - 272
1234