Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

被引：2
作者：
de Gouw, Stijn [1 ,2 ]
de Boer, Frank [1 ,3 ]
Ahrendt, Wolfgang [4 ]
Bubel, Richard [5 ]
机构：
[1] CWI, Amsterdam, Netherlands
[2] SDL Fredhopper, Amsterdam, Netherlands
[3] Leiden Univ, Amsterdam, Netherlands
[4] Chalmers Univ Technol, Gothenburg, Sweden
[5] Tech Univ Darmstadt, Dept Comp Sci, Darmstadt, Germany
来源：
SOFTWARE AND SYSTEMS MODELING | 2016年 / 15卷 / 04期
关键词：
Specification; Verification; Program logic; Dynamic logic; Object creation; ORIENTED PROGRAMS; !text type='JAVA']JAVA[!/text; PARALLEL;
D O I：
10.1007/s10270-014-0446-9
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.
引用
收藏
页码：1117 / 1140
页数：24
相关论文
共 51 条
[1]  
Abadi M., 1997, TAPSOFT '97: Theory and Practice of Software Development. 7th International Joint Conference CAAP/FASE. Proceedings, P682, DOI 10.1007/BFb0030634
[2]  
Abrahám E, 2008, FUND INFORM, V82, P391
[3]  
Ahrendt W, 2012, PROCEEDINGS OF THE 10TH INTERNATIONAL WORKSHOP ON JAVA TECHNOLOGIES FOR REAL-TIME AND EMBEDDED SYSTEMS, P145
[4]  
Ahrendt W, 2009, LECT NOTES COMPUT SC, V5850, P612, DOI 10.1007/978-3-642-05089-3_39
[5]  
AMERICA P, 1991, LECT NOTES COMPUT SC, V527, P1
[6]  
America P., 1990, REX WORKSH, P60
[7]  
[Anonymous], 2001, FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, DOI DOI 10.1007/3-540-45294-X10
[8]   10 YEARS OF HOARE LOGIC - A SURVEY .1. [J].
APT, KR .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1981, 3 (04) :431-483
[9]   Verification of object-oriented programs: A transformational approach [J].
Apt, Krzysztof R. ;
de Boer, Frank S. ;
Olderog, Ernst-Ruediger ;
de Gouw, Stijn .
JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2012, 78 (03) :823-852
[10]  
Apt Krzysztof R., 2009, VERIFICATION SEQUENT, V3, DOI [DOI 10.1007/978-1-84882-745-5, 10.1007/978-1-84882-745-5]
123456