Peter Müller - Specification and Verification of Closures
Event details
| Date | 30.03.2010 |
| Hour | 16:15 |
| Speaker | Peter Müller (ETH Zürich) |
| Location |
INM 010
|
| Category | Conferences - Seminars |
Closures, first-class citizen procedures that are able to capture their lexical environment, increase the expressiveness of object-oriented languages such as C#, Scala, and various dynamic languages. However, closures make program specification and verification more difficult. For instance, a verification methodology must allow specifications to describe the behavior of one method relatively to the specification of another method passed as argument, and it must allow specifications to describe the behavior of a closure without exposing its captured state. This paper presents a modular specification and verification methodology for closures. Our solution is based on first-order logic and, thus, well suited for automatic verification with SMT solvers. We have verified a series of interesting examples that cover the main applications of closures such as delegation patterns and even the creation of custom control flow.
Links
Practical information
- General public
- Free
Contact
- Viktor Kuncak