2026-07-23T21:24:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4870 2024-03-06T10:35:28Z ddc:004 open_access

Summary-Based Inter-Procedural Analysis via Modular Trace Refinement Cassez, Franck Müller, Christian Burnett, Karla Program verification Hoare Logic Refinement Automata 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Franck Cassez and Christian Müller and Karla Burnett 2014 Is Part Of LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2014.545 urn:nbn:de:0030-drops-48708 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.545 eng https://creativecommons.org/licenses/by/3.0/legalcode