DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2014.545

Summary-Based Inter-Procedural Analysis via Modular Trace Refinement

Authors: Franck Cassez, Christian Müller, and Karla Burnett

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract

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.

Cite as

Franck Cassez, Christian Müller, and Karla Burnett. Summary-Based Inter-Procedural Analysis via Modular Trace Refinement. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 545-556, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{cassez_et_al:LIPIcs.FSTTCS.2014.545,
  author =	{Cassez, Franck and M\"{u}ller, Christian and Burnett, Karla},
  title =	{{Summary-Based Inter-Procedural Analysis via Modular Trace Refinement}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{545--556},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.545},
  URN =		{urn:nbn:de:0030-drops-48708},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.545},
  annote =	{Keywords: Program verification, Hoare Logic, Refinement, Automata}
}

Search Results

Documents authored by Müller, Christian

Summary-Based Inter-Procedural Analysis via Modular Trace Refinement

Abstract

Cite as

Thanks for your feedback!

Could not send message