Advertisement

CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation

(Competition Contribution)
  • Yu-Fang Chen
  • Chiao Hsieh
  • Ming-Hsien Tsai
  • Bow-Yaw Wang
  • Farn Wang
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)

Abstract

CPArec is a tool for verifying recursive C programs via source-to-source program transformation. It uses a recursion-free program analyzer CPAChecker as a black box and computes function summaries from the inductive invariants generated by CPAChecker. Such function summaries enable CPArec to check recursive programs.

References

  1. 1.
    Beyer, D., Keremoglu, M.E.: cPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011)Google Scholar
  2. 2.
    Chen, Y.-F., Hsieh, C., Tsai, M.-H., Wang, B.-Y., Wang, F.: Verifying recursive programs using intraprocedural analyzers. In: Müller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 118–133. Springer, Heidelberg (2014)Google Scholar
  3. 3.
    Clarke, E.M.: Program invariants as fixed points. In: 18th Annual Symposium on Foundations of Computer Science, pp. 18–29. IEEE (1977)Google Scholar
  4. 4.
    Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol. 2304, p. 213. Springer, Heidelberg (2002)Google Scholar
  5. 5.

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Yu-Fang Chen
    • 1
  • Chiao Hsieh
    • 1
    • 2
  • Ming-Hsien Tsai
    • 1
  • Bow-Yaw Wang
    • 1
  • Farn Wang
    • 2
  1. 1.Institute of Information ScienceAcademia SinicaTaipeiTaiwan
  2. 2.Graduate Institute of Electrical EngineeringNational Taiwan UniversityTaipeiTaiwan

Personalised recommendations