Summary-based inter-procedural analysis via modular trace refinement

Franck Cassez, Christian Müller, Karla Burnett

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

6 Citations (Scopus)
3 Downloads (Pure)

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.

Original languageEnglish
Title of host publication34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014
EditorsVenkatesh Raman, S. P. Suresh
Place of PublicationDagstuhl, Germany
PublisherDagstuhl Publishing
Pages545-556
Number of pages12
Volume29
ISBN (Electronic)9783939897774
DOIs
Publication statusPublished - 1 Dec 2014
Externally publishedYes
Event34th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014 - New Delhi, India
Duration: 15 Dec 201417 Dec 2014

Other

Other34th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014
CountryIndia
CityNew Delhi
Period15/12/1417/12/14

Bibliographical note

Copyright the Author(s). Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

Keywords

  • automata
  • Hoare logic
  • program verification
  • refinement

Fingerprint

Dive into the research topics of 'Summary-based inter-procedural analysis via modular trace refinement'. Together they form a unique fingerprint.

Cite this