2011: Samin Ishtiaq and Peter W. O'Hearn

(for 2001) BI as an Assertion Language for Mutable Data Structures


In applying the logic of bunched implications (BI) to mutable data structures this paper laid the groundwork for the flowering of separation logic (heap models of separation logic are specific BI models), which allows reasoning about programs with dynamically allocated (and deallocated) memory. This paper introduced the 'frame rule' which supports local reasoning in separation logic, where specifications and proofs concentrate on just those memory cells manipulated by a program component rather than the entire global program state. Separation logic underlies continuing research on what is described as local reasoning, having diverse application in domains such as program verification and automated parallelization.