COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

## Linear mapsAdd to your list(s) Download to your calendar using vCal - David Walker (visiting from Princeton)
- Monday 28 June 2010, 12:45-14:00
- Room FW26, Computer Laboratory, William Gates Building.
If you have a question about this talk, please contact Sam Staton. 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, 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! This talk is part of the Semantics Lunch (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory talks
- Interested Talks
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsSpecial DPMMS Colloquium Market Square: Cambridge Business and Society Interdisciplinary Research Group Cambridge Global Health Year## Other talksMechanical performance of wall structures in 3D printing processes: theory, design tools and experiments South American Opuntioids What is the History of the Book? From dry to wet granular media Research frontiers and new therapeutic strategies in pancreatic cancer Graph Convolutional Networks for Natural Language Processing and Relational Modeling |