We propose a generalisation of trace refinement for the verification of inter-procedural programs. Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the main features of our approach and yields promising results.
|Title of host publication||34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014|
|Editors||Venkatesh Raman, S. P. Suresh|
|Place of Publication||Dagstuhl, Germany|
|Number of pages||12|
|Publication status||Published - 1 Dec 2014|
|Event||34th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014 - New Delhi, India|
Duration: 15 Dec 2014 → 17 Dec 2014
|Other||34th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014|
|Period||15/12/14 → 17/12/14|
Bibliographical noteCopyright the Author(s). Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.
- Hoare logic
- program verification