TY - GEN

T1 - Linear maps

AU - Lahiri, Shuvendu K.

AU - Qadeer, Shaz

AU - Walker, David P.

PY - 2011/3/7

Y1 - 2011/3/7

N2 - Verification of large programs is impossible without proof techniques that allow local reasoning and information hiding. In this paper, we take the approach of modeling the heap as a collection of partial functions with disjoint domains. We call each such partial function a linear map. Programmers may select objects from linear maps, update linear maps or transfer addresses and their contents from one linear map to another. Programmers may also declare new linear map variables and pass linear maps as arguments to procedures. The program logic prevents any of these operations from duplicating locations and thereby breaking the key heap representation invariant: the domains of all linear maps remain disjoint. Linear maps facilitate modular reasoning because programs that use them are also able to use simple, classical frame rules to preserve information about heap state across procedure calls. We illustrate our approach through examples, prove that our verification rules are sound, and show that operations on linear maps may be erased and replaced by equivalent operations on a single, global heap.

AB - Verification of large programs is impossible without proof techniques that allow local reasoning and information hiding. In this paper, we take the approach of modeling the heap as a collection of partial functions with disjoint domains. We call each such partial function a linear map. Programmers may select objects from linear maps, update linear maps or transfer addresses and their contents from one linear map to another. Programmers may also declare new linear map variables and pass linear maps as arguments to procedures. The program logic prevents any of these operations from duplicating locations and thereby breaking the key heap representation invariant: the domains of all linear maps remain disjoint. Linear maps facilitate modular reasoning because programs that use them are also able to use simple, classical frame rules to preserve information about heap state across procedure calls. We illustrate our approach through examples, prove that our verification rules are sound, and show that operations on linear maps may be erased and replaced by equivalent operations on a single, global heap.

UR - http://www.scopus.com/inward/record.url?scp=79952176842&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79952176842&partnerID=8YFLogxK

U2 - 10.1145/1929529.1929531

DO - 10.1145/1929529.1929531

M3 - Conference contribution

AN - SCOPUS:79952176842

SN - 9781450304870

T3 - PLPV'11 - Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification

SP - 3

EP - 14

BT - PLPV'11 - Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification

T2 - 5th ACM Workshop on Programming Languages Meets Program Verification, PLPV 2011

Y2 - 29 January 2011 through 29 January 2011

ER -