Summary-Based Inter-Procedural Analysis via Modular Trace Refinement
Franck Cassez, Christian Müller, Karla Burnett · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2014
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.