Abstract
Verication of programs with invocations to unknown pro-
cedures is a practical problem, because in many scenarios not all codes
of programs to be veried are available. Those unknown calls also pose
a challenge for their verication. This paper addresses this problem with
an attempt to verify the full functional correctness of such programs
using pointer-based data structures. Provided with a Hoare-style speci-
cation fprg prog fpog where program prog contains calls to some un-
known procedure unknown, we infer a specication mspecu for unknown
from the calling contexts, such that the problem of verifying prog can
be safely reduced to the problem of proving that the procedure unknown
(once its code is available) meets the derived specication mspecu. The
expected specication mspecu for the unknown procedure unknown is au-
tomatically calculated using an abduction-based shape analysis speci-
cally designed for a combined abstract domain. We have also done some
experiments to validate the viability of our approach.
cedures is a practical problem, because in many scenarios not all codes
of programs to be veried are available. Those unknown calls also pose
a challenge for their verication. This paper addresses this problem with
an attempt to verify the full functional correctness of such programs
using pointer-based data structures. Provided with a Hoare-style speci-
cation fprg prog fpog where program prog contains calls to some un-
known procedure unknown, we infer a specication mspecu for unknown
from the calling contexts, such that the problem of verifying prog can
be safely reduced to the problem of proving that the procedure unknown
(once its code is available) meets the derived specication mspecu. The
expected specication mspecu for the unknown procedure unknown is au-
tomatically calculated using an abduction-based shape analysis speci-
cally designed for a combined abstract domain. We have also done some
experiments to validate the viability of our approach.
| Original language | English |
|---|---|
| Title of host publication | Formal Methods and Software Engineering |
| Publisher | Springer Verlag |
| Pages | 171-187 |
| ISBN (Print) | 9783642169007 |
| DOIs | |
| Publication status | Published - 17 Nov 2010 |
Publication series
| Name | Formal Methods and Software Engineering |
|---|---|
| Volume | 6447 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |