Name
Abstract | ||
|---|---|---|
Object-oriented programs are notable for making use of both higher-order abstractions and mutable, aliased state. Either feature alone is challenging for formal verification, and the combination yields very flexible program designs and correspondingly difficult verification problems. In this paper, we show how to formally specify and verify programs that use several common design patterns in concert. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1145/1481861.1481874 | TLDI |
Keywords | Field | DocType |
higher-order abstraction,aliased state,object-oriented program,correspondingly difficult verification problem,separation logic,flexible program design,common design pattern,combination yield,formal verification,program design,object oriented programming,design patterns,design pattern | Separation logic,Functional verification,Abstraction,Programming language,Computer science,Software design pattern,Theoretical computer science,High-level verification,Formal verification | Conference |
Citations | PageRank | References |
18 | 1.02 | 12 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Neelakantan R. Krishnaswami | 1 | 188 | 12.99 |
| Jonathan Aldrich | 2 | 1076 | 77.64 |
| Lars Birkedal | 3 | 1481 | 96.84 |
| Kasper Svendsen | 4 | 127 | 6.84 |
| Alexandre Buisse | 5 | 37 | 2.74 |