
Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs
Keywords: assume-guarantee reasoning; side-effect; mod-clauses; shape analysis; abstract interpretation; theorem prover;