Imperial College London
Alternate

ProfessorSophiaDrossopoulou

Faculty of Engineering, Department of Computing

Professor of Programming Languages
 
 
 
//

Contact

 

s.drossopoulou Website

 
 
//

Location

 

559Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Wood:2017:10.1007/978-3-662-54434-1_35,
author = {Wood, T and Drossopoulou, S and Lahiri, SK and Eisenbach, S},
doi = {10.1007/978-3-662-54434-1_35},
publisher = {Springer Verlag},
title = {Modular verification of procedure equivalence in the presence of memory allocation},
url = {http://dx.doi.org/10.1007/978-3-662-54434-1_35},
year = {2017}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - For most high level languages, two procedures are equivalentif they transform a pair of isomorphic stores to isomorphic stores. How-ever, tools for modular checking of such equivalence impose a strongercheck where isomorphism is strengthened to equality of stores. This re-sults in the inability to prove many interesting program pairs with re-cursion and dynamic memory allocation.In this work, we present RIE, a methodology to modularly establishequivalence of procedures in the presence of memory allocation, cyclicdata structures and recursion. Our technique addresses the need for find-ing witnesses to isomorphism with angelic allocation, supports reasoningabout equivalent procedures calls when the stores are only locally iso-morphic, and reasoning about changes in the order of procedure calls.We have implemented RIE by encoding it in the Boogie program verifier.We describe the encoding and prove its soundness.
AU  - Wood,T
AU  - Drossopoulou,S
AU  - Lahiri,SK
AU  - Eisenbach,S
DO  - 10.1007/978-3-662-54434-1_35
PB  - Springer Verlag
PY  - 2017///
SN  - 0302-9743
TI  - Modular verification of procedure equivalence in the presence of memory allocation
UR  - http://dx.doi.org/10.1007/978-3-662-54434-1_35
UR  - http://hdl.handle.net/10044/1/43956
ER  -
Download