Abstract

Over the last decade, separation logic has risen to the top of the charts. When I arrived at Microsoft Research Redmond last fall for a sabbatical from Princeton, Shaz Qadeer and Shuvendu Lahiri ask why? Why are so many researchers so excited about this new advance? And, they asked, can we get what they’ve got?

These questions led us to try to capture the spirit of the separation logic proof strategy in a classical first-order theorem proving environment. To be more specific, we sought a conservative extension of Boogie, which is a classical verification condition generator for imperative programs, that would admit the use of effective frame and anti-frame rules and thereby allow the kinds of modular proofs that make separation logic so attractive. However, we did not want to have to change the underlying theorem proving technology, so any verification conditions generated would have to be ordinary first-order logic formulae over terms from well supported theories such as the theories of arrays, sets and arithmetic. Moreover, in order for our theorem prover, Z3, to be able to discharge the verification conditions effectively, it was essential that they contain no more quantifiers than normal.

In this informal whiteboard talk, I will explain our solution to the problem, which is to add a new data type called a “linear map” to Boogie. Linear maps seem to have a number of very nice properties:

• the ideas are simple: I hope means other researchers will have an easy time building on them.

• verification conditions for operations on linear maps can be expressed in first-order logic using the theories of arrays, sets and arithmetic

• they work: we have used Boogie, Z3 and linear maps to mechanically verify classic examples drawn from past papers on separation logic.

If you want to find out what linear maps actually are, you’ll have to come to the talk!