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

详细信息    查看全文

• 作者：Yu-Fang Chen (15)
  Chiao Hsieh (15) (16)
  Ming-Hsien Tsai (15)
  Bow-Yaw Wang (15)
  Farn Wang (16)
  
  15. Institute of Information Science ; Academia Sinica ; Taipei ; Taiwan
  16. Graduate Institute of Electrical Engineering ; National Taiwan University ; Taipei ; Taiwan
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9035
• 期：1
• 页码：426-428
• 全文大小：104 KB
• 参考文献：1. Beyer, D., Keremoglu, M.E. cPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. eds. (2011) Computer Aided Verification. Springer, Heidelberg, pp. 184-190
  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. (2014) Static Analysis. Springer, Heidelberg, pp. 118-133
  3. Clarke, E.M.: Program invariants as fixed points. In: 18th Annual Symposium on Foundations of Computer Science, pp. 18鈥?9. IEEE (1977)
  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. eds. (2002) Compiler Construction. Springer, Heidelbergpp. 213
  5. Redlog, http://www.redlog.eu/
  
• 作者单位：Tools and Algorithms for the Construction and Analysis of Systems
• 丛书名：978-3-662-46680-3
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

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.