Name
Abstract | ||
|---|---|---|
We study automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls or code pointers. Given the specification of a procedure whose body contains calls to an unknown procedure, we try to infer the possible specifications for the unknown procedure from its calling contexts. We employ a forward shape analysis with separation logic and an abductive inference mechanism to synthesize both preand postconditions for the unknown procedure. The inferred specification is a partial specification of the unknown procedure. Therefore it is subject to a later verification when the code or the complete specification for the unknown procedure are available. Our inferred specifications can also be used for program understanding. |
Year | Venue | Field |
|---|---|---|
2010 | WING@ETAPS/IJCAR | Pointer (computer programming),Separation logic,Programming language,Unknown procedure,Work in process,Abductive reasoning,Engineering,Management science,Shape analysis (digital geometry) |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Florin Craciun | 1 | 40 | 8.19 |
| Chenguang Luo | 2 | 56 | 5.63 |
| Guanhua He | 3 | 68 | 7.50 |
| Shengchao Qin | 4 | 711 | 62.81 |
| Wei-Ngan Chin | 5 | 868 | 63.37 |