Summary-based inter-procedural analysis via modular trace refinement

Franck Cassez; Christian Müller; Karla Burnett

doi:10.4230/LIPIcs.FSTTCS.2014.545

Summary-based inter-procedural analysis via modular trace refinement

Franck Cassez, Christian Müller, Karla Burnett

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

6 Citations (Scopus)

22 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 language	English
Title of host publication	34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014
Editors	Venkatesh Raman, S. P. Suresh
Place of Publication	Dagstuhl, Germany
Publisher	Dagstuhl Publishing
Pages	545-556
Number of pages	12
Volume	29
ISBN (Electronic)	9783939897774
DOIs	https://doi.org/10.4230/LIPIcs.FSTTCS.2014.545
Publication status	Published - 1 Dec 2014
Externally published	Yes
Event	34th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014 - New Delhi, India Duration: 15 Dec 2014 → 17 Dec 2014

Other

Other	34th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014
Country/Territory	India
City	New Delhi
Period	15/12/14 → 17/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

Access to Document

10.4230/LIPIcs.FSTTCS.2014.545

Publisher version (open access)Final published version, 641 KBLicence: CC BY

Cite this

@inproceedings{0e389a04badc4041bf721eb9857cdaaf,

title = "Summary-based inter-procedural analysis via modular trace refinement",

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.",

keywords = "automata, Hoare logic, program verification, refinement",

author = "Franck Cassez and Christian M{\"u}ller and Karla Burnett",

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.; 34th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014 ; Conference date: 15-12-2014 Through 17-12-2014",

year = "2014",

month = dec,

day = "1",

doi = "10.4230/LIPIcs.FSTTCS.2014.545",

language = "English",

volume = "29",

pages = "545--556",

editor = "Venkatesh Raman and Suresh, \{S. P.\}",

booktitle = "34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014",

publisher = "Dagstuhl Publishing",

address = "Germany",

}

Cassez, F, Müller, C & Burnett, K 2014, Summary-based inter-procedural analysis via modular trace refinement. in V Raman & SP Suresh (eds), 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014. vol. 29, Dagstuhl Publishing, Dagstuhl, Germany, pp. 545-556, 34th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014, New Delhi, India, 15/12/14. https://doi.org/10.4230/LIPIcs.FSTTCS.2014.545

Summary-based inter-procedural analysis via modular trace refinement. / Cassez, Franck; Müller, Christian; Burnett, Karla.
34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014. ed. / Venkatesh Raman; S. P. Suresh. Vol. 29 Dagstuhl, Germany: Dagstuhl Publishing, 2014. p. 545-556.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Summary-based inter-procedural analysis via modular trace refinement

AU - Cassez, Franck

AU - Müller, Christian

AU - Burnett, Karla

N1 - 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.

PY - 2014/12/1

Y1 - 2014/12/1

N2 - 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.

AB - 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.

KW - automata

KW - Hoare logic

KW - program verification

KW - refinement

UR - https://www.scopus.com/pages/publications/84921444925

U2 - 10.4230/LIPIcs.FSTTCS.2014.545

DO - 10.4230/LIPIcs.FSTTCS.2014.545

M3 - Conference proceeding contribution

AN - SCOPUS:84921444925

VL - 29

SP - 545

EP - 556

BT - 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014

A2 - Raman, Venkatesh

A2 - Suresh, S. P.

PB - Dagstuhl Publishing

CY - Dagstuhl, Germany

T2 - 34th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014

Y2 - 15 December 2014 through 17 December 2014

ER -

Summary-based inter-procedural analysis via modular trace refinement

Abstract

Other

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this