Name
Abstract | ||
|---|---|---|
One promising approach to verifying heap-manipulating programs is based on user-definedinductive predicates in separation logic. This approach can describe data structures with complex invariants and sound reasoning based on unfold/fold. However, an important component towards more expressive program verification is the use of lemmasthat can soundly relate predicates beyond their original definitions. This paper outlines a new automaticmechanism for proving and applying user-specified lemmasunder separation logic. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-70545-1_34 | CAV |
Keywords | Field | DocType |
original definition,complex invariants,enhancing program verification,expressive program verification,promising approach,separation logic,heap-manipulating program,data structure,new automaticmechanism,important component,user-specified lemmasunder separation logic,entailment | Data structure,Separation logic,Logical consequence,Programming language,Computer science,Algorithm,Theoretical computer science,Invariant (mathematics),Predicate (grammar),Lemma (mathematics) | Conference |
Volume | ISSN | Citations |
5123 | 0302-9743 | 34 |
PageRank | References | Authors |
1.20 | 22 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Huu Hai Nguyen | 1 | 382 | 15.66 |
| Wei-Ngan Chin | 2 | 868 | 63.37 |