Relational separation logic

被引：77
作者：
Yang, Hongseok [1 ]
机构：
[1] Queen Mary Univ London, Dept Comp Sci, London, England
来源：
THEORETICAL COMPUTER SCIENCE | 2007年 / 375卷 / 1-3期
关键词：
separation logic; program verification; relational reasoning; Schorr-Waite graph marking algorithm;
D O I：
10.1016/j.tcs.2006.12.036
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper, we present a Hoare-style logic for specifying and verifying how two pointer programs are related. Our logic lifts the main features of separation logic, from an assertion to a relation, and from a property about a single program to a relationship between two programs. We show the strength of the logic, by proving that the Schorr-Waite graph marking algorithm is equivalent to the depth-first traversal. (c) 2007 Elsevier B.V. All rights reserved.
引用
收藏
页码：308 / 334
页数：27
相关论文
共 24 条
[1]  
Abrial JR, 2003, LECT NOTES COMPUT SC, V2805, P51
[2]  
Aho A., 1988, Compilers - Principles, Techniques and Tools
[3]  
[Anonymous], POPL 2001
[4]  
BENTON N, 2004, POPL, P14
[5]  
BIRKEDAL L, 2004, P 31 ACM SIGPLAN SIG, P220
[6]  
BORNAT R, 2004, P 2 WORSH SEM PROGR
[7]  
Calcagno Cristiano, 2001, FST TCS 2001, P108
[8]  
COLBY C, 2000, ACM SIGPLAN C PROGR
[9]  
Gardiner P. H. B., 1993, Formal Aspects of Computing, V5, P367, DOI 10.1007/BF01212407
[10]  
HE J, 1986, LECT NOTES COMPUT SC, V213, P187
123