Generating Specifications for Recursive Methods by Abstracting Program States

被引：2

作者：

Wasser, Nathan ^{[1
]}

机构：

[1] Tech Univ Darmstadt, Dept Comp Sci, Darmstadt, Germany

来源：

DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015 | 2015年 / 9409卷

关键词：

Program verification; Abstract interpretation; Specification generation; Method contracts; Recursion;

D O I：

10.1007/978-3-319-25942-0_16

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

In this paper we present a novel approach to automatically generate sound specifications for recursive methods. These specifications can help prove the absence of undesired behavior, provide programmers with a foundation to build upon and help locate implementation bugs. Our approach is based on symbolic execution which we use to determine the states of re-entry and exit points. From these we generalize the necessary pre-and postconditions using techniques from abstract interpretation. The presented approach has been prototypically implemented by integration into a faithful and precise program logic for sequential Java programs.

引用

页码：243 / 257

页数：15

共 19 条

[1] Ball T, 2001, LECT NOTES COMPUT SC, V2102, P260
[2] Ball T, 2000, LECT NOTES COMPUT SC, V1885, P113
[3] Beckert Bernhard., 2007, LNCS, V4334
[4] Bubel R, 2009, LECT NOTES COMPUT SC, V5751, P247
[5] Verifying recursive programs using intraprocedural analyzers
Chen, Yu-Fang
Hsieh, Chiao
Tsai, Ming-Hsien
Wang, Bow-Yaw
Wang, Farn
[J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8723 : 118 - 133
[6] Clarke EdmundM., 2000, Proceedings of the International Conference on Computer Aided Veri cation (CAV), P154, DOI 10.1007/1072216715
[7] Colón MA, 2003, LECT NOTES COMPUT SC, V2725, P420
[8] Cousot Patrick, 1977, POPL, DOI [10.1145/512950.512973, DOI 10.1145/512950.512973]
[9] The Daikon system for dynamic detection of likely invariants
Ernst, Michael D.
Perkins, Jeff H.
Guo, Philip J.
McCarnant, Stephen
Pacheco, Carlos
Tschantz, Matthew S.
Xiao, Chen
[J]. SCIENCE OF COMPUTER PROGRAMMING, 2007, 69 (1-3) : 35 - 45
[10] Flanagan C., 2001, FME 2001: Formal Methods for Increasing Software Productivity. International Symposium on Formal Methods Europe. Proceedings (Lecture Notes in Computer Science Vol.2021), P500

← 1 2 →