Relational interprocedural verification of concurrent programs

被引：0
作者：
Bertrand Jeannet
机构：
[1] INRIA,
来源：
Software & Systems Modeling | 2013年 / 12卷
关键词：
Concurrent program analysis; Interprocedural analysis; Abstract interpretation; Numerical abstract domains; Forward and backward analysis;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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
页数：21
相关论文
共 24 条
[1]  
Bryant R.E.(1986)Graph-based algorithms for boolean function manipulation IEEE Trans. Comput 35 377-183
[2]  
Caucal D.(1992)On the regular structure of prefix rewriting Theor. Comput. Sci 106 61-95
[3]  
Cousot P.(1992)Abstract interpretation and application to logic programs J. Logic Program 13 103-100
[4]  
Cousot R.(2005)Modular verification of multithreaded programs Theor. Comput. Sci 338 153-430
[5]  
Flanagan C.(2006)Some ways to reduce the space dimension in polyhedra computations Formal Methods Syst. Des 29 79-263
[6]  
Freund S.N.(2010)A relational approach to interprocedural shape analysis ACM Trans. Program. Lang. Syst. (TOPLAS) 32 5-298
[7]  
Qadeer S.(2006)The octagon abstract domain Higher-Order Symb. Comput 19 31-undefined
[8]  
Seshia S.A.(2000)Context-sensitive synchronization-sensitive analysis is undecidable ACM Trans. Program. Lang. Syst 22 416-undefined
[9]  
Halbwachs N.(2005)Weighted pushdown systems and their application to interprocedural dataflow analysis Sci. Comput. Program 58 206-undefined
[10]  
Merchat D.(2002)Parametric shape analysis via 3-valued logic ACM Trans. Prog. Lang. Syst 24 217-undefined
123