Name
Abstract | ||
|---|---|---|
Conventional specifications typically have a flat structure that is based primarily on the underlying logic. Such specifications lack structures that could have provided better guidance to the verification process. In this work, we propose to add three new structures to a specification framework for separation logic to achieve a more precise and better guided verification for pointer-based programs. The newly introduced structures empower users with more control over the verification process in the following ways: (i) case analysis can be invoked to take advantage of disjointness conditions in the logic. (ii) early, as opposed to late, instantiation can minimise on the use of existential quantification. (iii) formulae that are staged provide better reuse of the verification process. Initial experiments have shown that structured specifications can lead to more precise verification without incurring any performance overhead. |
Year | Venue | Keywords |
|---|---|---|
2011 | FM | conventional specification,underlying logic,case analysis,precise verification,disjointness condition,better verification,verification process,structured specification,separation logic,better reuse,existential quantification,better guidance,heap-manipulating program,verification |
Field | DocType | Citations |
Pointer (computer programming),Separation logic,Functional verification,Programming language,Software engineering,Computer science,Intelligent verification,Runtime verification,Real-time computing,Verification,High-level verification,Software verification | Conference | 10 |
PageRank | References | Authors |
0.66 | 19 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cristian Gherghina | 1 | 85 | 6.60 |
| Cristina David | 2 | 245 | 14.14 |
| Shengchao Qin | 3 | 711 | 62.81 |
| Wei-Ngan Chin | 4 | 868 | 63.37 |