1 Search Results for "Burnett, Karla"

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-dev.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}
}
  • Refine by Author
  • 1 Burnett, Karla
  • 1 Cassez, Franck
  • 1 Müller, Christian

  • Refine by Classification

  • Refine by Keyword
  • 1 Automata
  • 1 Hoare Logic
  • 1 Program verification
  • 1 Refinement

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2014

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact