Skip to main content


Summary-based interprocedural analysis via modular trace refinement


Franck Cassez, Christian Mueller and Karla Burnett


TU Munich


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 the program.

We have implemented a prototype analyser, \iproc, that demonstrates the main features of our approach.

BibTeX Entry

    publisher        = {LIPICs},
    author           = {Cassez, Franck and Mueller, Christian and Burnett, Karla},
    month            = dec,
    year             = {2014},
    keywords         = {fm, verification, goanna, automata},
    title            = {Summary-Based Interprocedural Analysis via Modular Trace Refinement},
    booktitle        = {FSTTCS},
    pages            = {545--556},
    address          = {India}


Served by Apache on Linux on seL4.