Document Open Access Logo

Summary-Based Inter-Procedural Analysis via Modular Trace Refinement

Authors Franck Cassez, Christian Müller, Karla Burnett

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2014.545.pdf
  • Filesize: 0.62 MB
  • 12 pages

Document Identifiers

Author Details

Franck Cassez
Christian Müller
Karla Burnett

Cite As Get BibTex

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) https://doi.org/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.

Subject Classification

Keywords
  • Program verification
  • Hoare Logic
  • Refinement
  • Automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Alex Aiken, Suhabe Bugrara, Isil Dillig, Thomas Dillig, Brian Hackett, and Peter Hawkins. An overview of the saturn project. In Manuvir Das and Dan Grossman, editors, PASTE, pages 43-48. ACM, 2007. Google Scholar
  2. Aws Albarghouthi, Arie Gurfinkel, and Marsha Chechik. Whale: An interpolation-based algorithm for inter-procedural verification. In Viktor Kuncak and Andrey Rybalchenko, editors, VMCAI, volume 7148 of LNCS, pages 39-55. Springer, 2012. Google Scholar
  3. Domagoj Babic and Alan J. Hu. Calysto: scalable and precise extended static checking. In Wilhelm Schäfer, Matthew B. Dwyer, and Volker Gruhn, editors, ICSE, pages 211-220. ACM, 2008. Google Scholar
  4. Thomas Ball, Vladimir Levin, and Sriram K. Rajamani. A decade of software model checking with SLAM. Commun. ACM, 54(7):68-76, 2011. Google Scholar
  5. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The software model checker Blast. STTT, 9(5-6):505-525, 2007. Google Scholar
  6. Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A Tool for Configurable Software Verification. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, CAV, volume 6806 of LNCS, pages 184-190. Springer, 2011. Google Scholar
  7. Sebastian Biallas, Mads Chr. Olesen, Franck Cassez, and Ralf Huuck. Ptrtracker: Pragmatic pointer analysis. In SCAM, pages 69-73. IEEE, 2013. Google Scholar
  8. Mark Bradley, Franck Cassez, Ansgar Fehnker, Thomas Given-Wilson, and Ralf Huuck. High performance static analysis for industry. ENTCS, 289:3-14, 2012. Google Scholar
  9. Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. SMTInterpol: An Interpolating SMT Solver. In Alastair F. Donaldson and David Parker, editors, SPIN, volume 7385 of LNCS, pages 248-254. Springer, 2012. Google Scholar
  10. William Craig. Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. J. Symb. Log., 22(3):269-285, 1957. Google Scholar
  11. Isil Dillig, Thomas Dillig, and Alex Aiken. Sound, complete and scalable path-sensitive analysis. In Rajiv Gupta and Saman P. Amarasinghe, editors, PLDI, pages 270-280. ACM, 2008. Google Scholar
  12. Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and SaiDeep Tetali. Compositional may-must program analysis: unleashing the power of alternation. In Hermenegildo and Palsberg [16], pages 43-56. Google Scholar
  13. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Refinement of trace abstraction. In Jens Palsberg and Zhendong Su, editors, SAS, volume 5673 of LNCS, pages 69-85. Springer, 2009. Google Scholar
  14. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Nested interpolants. In Hermenegildo and Palsberg [16], pages 471-482. Google Scholar
  15. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Software model checking for people who love automata. In Natasha Sharygina and Helmut Veith, editors, CAV, volume 8044 of LNCS, pages 36-52. Springer, 2013. Google Scholar
  16. Manuel V. Hermenegildo and Jens Palsberg, editors. Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. ACM, 2010. Google Scholar
  17. Thomas W. Reps, Susan Horwitz, and Shmuel Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 49-61, 1995. Google Scholar
  18. Ondrej Sery, Grigory Fedyukovich, and Natasha Sharygina. Interpolation-based function summaries in bounded model checking. In Kerstin Eder, João Lourenço, and Onn Shehory, editors, HVC, volume 7261 of LNCS, pages 160-175. Springer, 2011. Google Scholar
  19. Micha Sharir and Amir Pnueli. Two approaches to interprocedural data flow analysis. Technical report, 1978. Dpt. Of Computer Science, Courant Institute, NY, USA. Google Scholar
  20. Ultimate Automizer. URL: http://ultimate.informatik.uni-freiburg.de/automizer/.
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 About DROPS Imprint Privacy Contact