請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/54099完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 王凡(Farn Wang) | |
| dc.contributor.author | Chiao Hsieh | en |
| dc.contributor.author | 謝橋 | zh_TW |
| dc.date.accessioned | 2021-06-16T02:39:57Z | - |
| dc.date.available | 2015-07-24 | |
| dc.date.copyright | 2015-07-24 | |
| dc.date.issued | 2015 | |
| dc.date.submitted | 2015-07-22 | |
| dc.identifier.citation | [1] E. M. Clarke, H. Jain, and N. Sinha, “Grand challenge: model check software,” in Proc. the NATO Advanced Research Workshop on Verification of Infinite State Systems with Applications to Security (VISSAS 2005), Timi﹐soara, România, 2005, pp. 55–68.
[2] D. Beyer and M. E. Keremoglu, “CPAchecker: A tool for configurable software verification,” in Proc. CAV’11, Snowbird, UT, USA, 2011, pp. 184–190. [3] D. Beyer, “Status report on software verification - (competition summary SV-COMP 2014),” in Proc. TACAS’14, Grenoble, France, 2014, pp. 373–388. [Online]. Available: http://sv-comp.sosy-lab.org/2014/. [4] Y. Chen, C. Hsieh, M. Tsai, B. Wang, and F. Wang, “Verifying recursive programs using intraprocedural analyzers,” in Proc. SAS’14, Munich, Germany, 2014, pp. 118–133. [5] D. Beyer, “Software verification and verifiable witnesses - (report on SV-COMP 2015),” in Proc. TACAS’15, London, UK, 2015, pp. 401–416. [Online]. Available: http://sv-comp.sosy-lab.org/2015/. [6] Y. Chen, C. Hsieh, M. Tsai, B. Wang, and F. Wang, “CPArec: Verifying recursive programs via source-to-source program transformation - (competition contribution),” in Proc. TACAS’15, London, UK, 2015, pp. 426–428. [7] D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “The software model checker Blast,” Int. J. Software Tools for Technology Transfer, vol. 9, no. 5-6, pp. 505–525, Sep. 2007. [8] A. Albarghouthi, Y. Li, A. Gurfinkel, and M. Chechik, “Ufo: A framework for abstraction- and interpolation-based software verification,” in Proc. CAV’12, Berkeley, CA, USA, 2012, pp. 672–678. [9] T.W. Reps, S. Horwitz, and S. Sagiv, “Precise interprocedural dataflow analysis via graph reachability,” in Proc. POPL’95, San Francisco, CA, USA, 1995, pp. 49–61. [10] T. Ball and S. K. Rajamani, “The SLAM toolkit,” in Proc. CAV’01, Paris, France, 2001, pp. 260–264. [11] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival, “The ASTREÉ analyzer,” in Proc. ESOP’05, Edinburgh, UK, 2005, pp. 21–30. [12] P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, “Frama-C: A software analysis perspective,” in Proc. SEFM’12, Thessaloniki, Greece, 2012, pp. 233–247. [13] (2015). Coverity, Coverity, Inc., [Online]. Available: http://www.coverity.com/. [14] (2015). Polyspace, The MathWorks, Inc., [Online]. Available: http://www.mathworks.com/products/polyspace/. [15] E. M. Clarke, D. Kroening, and F. Lerda, “A tool for checking ANSI-C programs,” in Proc. TACAS’04, Barcelona, Spain, 2004, pp. 168–176. [16] M. Heizmann, J. Christ, D. Dietsch, E. Ermis, J. Hoenicke, M. Lindenmann, A. Nutz, C. Schilling, and A. Podelski, “Ultimate Automizer with SMTInterpol - (competition contribution),” in Proc. TACAS’13, Rome, Italy, 2013, pp. 641–643. [17] E. Ermis, A. Nutz, D. Dietsch, J. Hoenicke, and A. Podelski, “Ultimate Kojak - (competition contribution),” in Proc. TACAS’14, Grenoble, France, 2014, pp. 421– 423. [18] A. Albarghouthi, A. Gurfinkel, and M. Chechik, “Whale: An interpolation-based algorithm for inter-procedural verification,” in Proc. VMCAI’12, Philadelphia, PA, USA, 2012, pp. 39–55. [19] D. von Oheimb, “Hoare logic for mutual recursion and local variables,” in Proc. FSTTCS, Chennai, India, 1999, pp. 168–180. [20] A. Lal and T. W. Reps, “Reducing concurrent analysis under a context bound to sequential analysis,” in Proc. CAV’08, Princeton, NJ, USA, 2008, pp. 37–51. [21] ——, “Reducing concurrent analysis under a context bound to sequential analysis,” Formal Methods in System Design, vol. 35, no. 1, pp. 73–97, Aug. 2009. [22] F. Nielson, H. R. Nielson, and C. Hankin, Principles of Program Analysis. Secaucus, NJ, USA: Springer-Verlag, 1999. [23] T. Ball and S. K. Rajamani, “Bebop: A symbolic model checker for boolean programs,” in Proc. SPIN, Stanford, CA, USA, 2000, pp. 113–130. [24] Z. Manna and A. Pnueli, “Formalization of properties of functional programs,” J. ACM, vol. 17, no. 3, pp. 555–569, Jul. 1970. [25] H. R. Nielson and F. Nielson, Semantics with Applications: An Appetizer, ser. Undergraduate Topics in Computer Science. London, UK: Springer-Verlag, 2007. [26] G. Tan and A. W. Appel, “A compositional logic for control flow,” in Proc. VMCAI’06, Charleston, SC, USA, 2006, pp. 80–94. [27] G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer, “CIL: Intermediate language and tools for analysis and transformation of C programs,” in Proc. CC’02, Grenoble, France, 2002, pp. 213–228. [28] (2015). C Intermediate Language, [Online]. Available: http://kerneis.github.io/cil/. [29] A. Dolzmann and T. Sturm, “REDLOG: Computer algebra meets computer logic,” SIGSAM Bull., vol. 31, no. 2, pp. 2–9, Jun. 1997. [30] (2015). Redlog, [Online]. Available: http://www.redlog.eu/. [31] M. Dangl, S. Löwe, and P. Wendler, “CPAchecker with support for recursive programs and floating-point arithmetic - (competition contribution),” in Proc. TACAS’15, London, UK, 2015, pp. 423–425. [32] J. C. Reynolds, “Separation Logic: A logic for shared mutable data structures,” in Proc. LICS’02, Copenhagen, Denmark, 2002, pp. 55–74. [33] S. Magill, M. Tsai, P. Lee, and Y. Tsay, “THOR: A tool for reasoning about shape and arithmetic,” in Proc. CAV’08, Princeton, NJ, USA, 2008, pp. 428–432. [34] Proc. 20th Int. Conf. Computer Aided Verification (CAV’08), Princeton, NJ, USA, 2008. [35] Proc. 21st Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15), London, UK, 2015. [36] Proc. 20th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14), Grenoble, France, 2014. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/54099 | - |
| dc.description.abstract | 在程序分析(Program Analysis) 領域中，分析遞迴程式(Recursive Program) 是一項難以處理的課題。現有程式分析工具往往因為無法處理程式中的遞迴函式，既而忽略部分程式碼不進行分析，或甚至拒絕檢驗遞迴程式。本篇論文針對遞迴程式的分析提出新的觀點與分析方法；作者認為與其重新設計演算法且實作新的分析器，不如改進現有的程式分析工具。但更改他人實作的軟體工具並非易事，因此本文提出的方法將現有的工具視為黑箱不做任何更動，反而是利用程式變換方法(Program Transformation) 將待分析的遞迴程式轉換成無遞迴的程式，再交給黑箱分析工具進行檢驗；並使用黑箱工具提供被分析程式中的不變量(Invariants)，進而證明原遞迴程式的正確性。
本篇作者與實驗室團隊受惠於程式分析工具CPAchecker，實作出此演算法的雛型CPArec，且參與2015年度軟體驗證競賽(Competition on Software Verification)；和其它頂尖實驗室所開發工具相較，我們的工具針對遞迴程式進行分析時，亦表現出相當的效率及效能，獲得第三名的佳績。 關鍵字：軟體驗證、程序分析、靜態分析、遞迴程式、程式變換方法 | zh_TW |
| dc.description.abstract | Recursion can complicate program analysis significantly. Some program analyzers simply ignore recursion or even refuse to check recursive programs. In this paper, we propose an algorithm that uses a recursion-free program analyzer as a black box to check recursive programs. With extended program constructs for assumptions, assertions, and non-deterministic values, our algorithm computes function summaries from inductive invariants computed by the underlying program analyzer. Such function summaries enable our algorithm to check recursive programs. We implement a prototype named CPArec using the recursion-free program analyzer CPAchecker. Under the comparison with other program analyzers on the benchmarks in the 2014 and 2015 Competitions on Software Verification, our tool shows competitive efficiency and effectiveness on verifying programs with recursion.
Key words: CPArec, Software Verification, Program Analysis, Static Analysis, Recursion, Program Transformation | en |
| dc.description.provenance | Made available in DSpace on 2021-06-16T02:39:57Z (GMT). No. of bitstreams: 1 ntu-104-R02943142-1.pdf: 1807815 bytes, checksum: 541b3b9bed6b377396ca33aa413f9c61 (MD5) Previous issue date: 2015 | en |
| dc.description.tableofcontents | 口試委員會審定書 i
Oral Examination Approval Form ii Acknowledgements iii 摘要 iv Abstract v 1 Introduction 1 2 Related Works 4 3 Preliminaries 5 3.1 Program Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Hoare Logic and Program Analysis . . . . . . . . . . . . . . . . . . . . . 7 4 Overview 9 5 Proving via Transformation 13 5.1 Unwinding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.1.1 Function Inlining Method . . . . . . . . . . . . . . . . . . . . . 14 5.1.2 Function Duplicating Method . . . . . . . . . . . . . . . . . . . 15 5.2 Under-approximation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 5.2.1 Approximating Functions . . . . . . . . . . . . . . . . . . . . . 18 5.2.2 Approximating Programs from Function Inlining Method . . . . . 19 5.2.3 Approximating Programs from Function Duplicating Method . . 19 5.3 Computing Summaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.4 Checking Summaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 5.5 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6 Experiments 26 6.1 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 6.2 Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 7 Conclusion 32 | |
| dc.language.iso | en | |
| dc.subject | 程序分析 | zh_TW |
| dc.subject | 軟體驗證 | zh_TW |
| dc.subject | 靜態分析 | zh_TW |
| dc.subject | 遞迴程式 | zh_TW |
| dc.subject | 程式變換方法 | zh_TW |
| dc.subject | 軟體驗證 | zh_TW |
| dc.subject | 程序分析 | zh_TW |
| dc.subject | 靜態分析 | zh_TW |
| dc.subject | 遞迴程式 | zh_TW |
| dc.subject | 程式變換方法 | zh_TW |
| dc.subject | Static Analysis | en |
| dc.subject | Software Verification | en |
| dc.subject | CPArec | en |
| dc.subject | Program Transformation | en |
| dc.subject | Recursion | en |
| dc.subject | Static Analysis | en |
| dc.subject | Program Analysis | en |
| dc.subject | Program Transformation | en |
| dc.subject | Recursion | en |
| dc.subject | CPArec | en |
| dc.subject | Software Verification | en |
| dc.subject | Program Analysis | en |
| dc.title | 以程式變換方法協助程式分析器驗證遞迴程式 | zh_TW |
| dc.title | Verifying Recursive Program via Source-to-Source Program Transformation | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 103-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 王柏堯(Bow-Yaw Wang),戴顯權(Shen-Chuan Tai),江介宏(Jie-Hong Jiang),陳郁方(Yu-Fang Chen) | |
| dc.subject.keyword | 軟體驗證,程序分析,靜態分析,遞迴程式,程式變換方法, | zh_TW |
| dc.subject.keyword | CPArec,Software Verification,Program Analysis,Static Analysis,Recursion,Program Transformation, | en |
| dc.relation.page | 38 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2015-07-23 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
| 顯示於系所單位： | 電子工程學研究所 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-104-1.pdf 未授權公開取用 | 1.77 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。