@inproceedings{fsttcs-14,
  author    = {Franck Cassez and
               Christian Müller and
               Karla Burnett},
  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, December 15-17, 2014,
               New Delhi, India},
  pages     = {545--556},
  year      = {2014},
  mywebpage = {soft-verif},
  category = {Software verification},
  keywords = {trace refinement, software verification, Hoare logic},
  url_link       = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545},
  doi       = {10.4230/LIPIcs.FSTTCS.2014.545},
  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.
  },
  Type = {B - International Conferences},
}

{"_id":"WDXeB8EXbDqsDca8k","bibbaseid":"cassez-mller-burnett-summarybasedinterproceduralanalysisviamodulartracerefinement-2014","author_short":["Cassez, F.","Müller, C.","Burnett, K."],"bibdata":{"bibtype":"inproceedings","type":"B - International Conferences","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Christian"],"propositions":[],"lastnames":["Müller"],"suffixes":[]},{"firstnames":["Karla"],"propositions":[],"lastnames":["Burnett"],"suffixes":[]}],"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, December 15-17, 2014, New Delhi, India","pages":"545–556","year":"2014","mywebpage":"soft-verif","category":"Software verification","keywords":"trace refinement, software verification, Hoare logic","url_link":"http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545","doi":"10.4230/LIPIcs.FSTTCS.2014.545","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. ","bibtex":"@inproceedings{fsttcs-14,\n author = {Franck Cassez and\n Christian Müller and\n Karla Burnett},\n title = {Summary-Based Inter-Procedural Analysis via Modular Trace Refinement},\n booktitle = {34th International Conference on Foundation of Software Technology\n and Theoretical Computer Science, {FSTTCS} 2014, December 15-17, 2014,\n New Delhi, India},\n pages = {545--556},\n year = {2014},\n mywebpage = {soft-verif},\n category = {Software verification},\n keywords = {trace refinement, software verification, Hoare logic},\n url_link = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545},\n doi = {10.4230/LIPIcs.FSTTCS.2014.545},\n abstract = {We propose a generalisation of trace refinement for the verification of inter-procedural programs.\n Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand\n and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a\n modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the\n main features of our approach and yields promising results.\n },\n Type = {B - International Conferences},\n}\n\n\n","author_short":["Cassez, F.","Müller, C.","Burnett, K."],"key":"fsttcs-14","id":"fsttcs-14","bibbaseid":"cassez-mller-burnett-summarybasedinterproceduralanalysisviamodulartracerefinement-2014","role":"author","urls":{" link":"http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545"},"keyword":["trace refinement","software verification","Hoare logic"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":["trace refinement","software verification","hoare logic"],"search_terms":["summary","based","inter","procedural","analysis","via","modular","trace","refinement","cassez","müller","burnett"],"title":"Summary-Based Inter-Procedural Analysis via Modular Trace Refinement","year":2014}