A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9364
• 期：1
• 页码：64-79
• 全文大小：1,148 KB
• 参考文献：1.Binkley, D.: Using semantic differencing to reduce the cost of regression testing. In: Proceedings of Conference on Software Maintenance, pp. 41–50, November 1992
  2.Brumley, D., Poosankam, P., Song, D., Zheng, J.: Automatic patch-based exploit generation is possible: Techniques and implications. In: 2008 IEEE Symposium on Security and Privacy (SP 2008), pp. 143–157. IEEE Computer Society (2008)
  3.Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252. ACM Press (1977)
  4. Gao, D., Reiter, M.K., Song, D.: BinHunt: automatically finding semantic differences in binary programs. In: Chen, L., Ryan, M.D., Wang, G. (eds.) ICICS 2008. LNCS, vol. 5308, pp. 238–255. Springer, Heidelberg (2008) CrossRef
  5.Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRef MATH
  6.Horwitz, S.: Identifying the semantic and textual differences between two versions of a program. SIGPLAN Not. 25(6), 234–245 (1990)MathSciNet CrossRef
  7.Jackson, D., Ladd, D.A.: Semantic diff: A tool for summarizing the effects of modifications. In: Proceedings of the International Conference on Software Maintenance (ICSM 1994), pp. 243–252, Washington, DC. IEEE Computer Society (1994)
  8. Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712–717. Springer, Heidelberg (2012) CrossRef
  9.Lahiri, S.K., Vaswani, K., Hoare, C.A.R.: Differential static analysis: opportunities, applications, and challenges. In: Proceedings of the FSE/SDP Workshop on Future of Software Engineering Research (FoSER 2010), pp. 201–204, ACM. New York (2010)
  10.Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef
  11.The Coq development team: The Coq proof assistant reference manual. LogiCal Project. Version 8.0 (2004)
  12. Partush, N., Yahav, E.: Abstract semantic differencing for numerical programs. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 238–258. Springer, Heidelberg (2013) CrossRef
  13.Partush, N., Yahav, E.: Abstract semantic differencing via speculative correlation. In: ACM International Conference on Object Oriented Programming Systems Languages and Applications(OOPSLA 2014), pp. 811–828, ACM. New York (2014)
  14.Person, S., Dwyer, M.B., Elbaum, S., Pǎsǎreanu, C.S.: Differential symbolic execution. In: 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering(SIGSOFT 2008/FSE-16), pp. 226–237, ACM (2008)
  15. Strichman, O., Godlin, B.: Regression verification - a practical way to verify programs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 496–501. Springer, Heidelberg (2008) CrossRef
  16.Yang, G., Person, S., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. ACM Trans. Softw. Eng. Methodol. 24(1), 3:1–3:42 (2014)CrossRef
  
• 作者单位：Thibaut Girka (16) (17)
  David Mentré (16)
  Yann Régis-Gianas (17)
  
  16. Mitsubishi Electric R&D Centre Europe, 35708, Rennes, France
  17. University of Paris Diderot, Sorbonne Paris Cité, PPS, UMR 7126 CNRS, PiR2, INRIA Paris-Rocquencourt, 75205, Paris, France
  
• 丛书名：Automated Technology for Verification and Analysis
• ISBN：978-3-319-24953-7
• 刊物类别：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

文摘

We present a new algorithm for the construction of a correlating program from the syntactic difference between the original and modified versions of a program. This correlating program exhibits the semantics of the two input programs and can then be used to compute their semantic differences, following an approach of Partush and Yahav [12]. We show that Partush and Yahav’s correlating program is unsound on loops that include an early exit. Our algorithm is defined on an imperative language with -loops, , and . To guarantee its correctness, it is formalized and mechanically checked within the Coq proof assistant. On a series of examples, we experimentally find that the static analyzer dizy is at least as precise on our correlating program as on Partush and Yahav’s. Page %P Close Plain text Look Inside Chapter Metrics Provided by Bookmetrix Reference tools Export citation EndNote (.ENW) JabRef (.BIB) Mendeley (.BIB) Papers (.RIS) Zotero (.RIS) BibTeX (.BIB) Add to Papers Other actions About this Book Reprints and Permissions Share Share this content on Facebook Share this content on Twitter Share this content on LinkedIn Supplementary Material (0) References (16) References1.Binkley, D.: Using semantic differencing to reduce the cost of regression testing. In: Proceedings of Conference on Software Maintenance, pp. 41–50, November 19922.Brumley, D., Poosankam, P., Song, D., Zheng, J.: Automatic patch-based exploit generation is possible: Techniques and implications. In: 2008 IEEE Symposium on Security and Privacy (SP 2008), pp. 143–157. IEEE Computer Society (2008)3.Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252. ACM Press (1977)4. Gao, D., Reiter, M.K., Song, D.: BinHunt: automatically finding semantic differences in binary programs. In: Chen, L., Ryan, M.D., Wang, G. (eds.) ICICS 2008. LNCS, vol. 5308, pp. 238–255. Springer, Heidelberg (2008) CrossRef5.Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefMATH6.Horwitz, S.: Identifying the semantic and textual differences between two versions of a program. SIGPLAN Not. 25(6), 234–245 (1990)MathSciNetCrossRef7.Jackson, D., Ladd, D.A.: Semantic diff: A tool for summarizing the effects of modifications. In: Proceedings of the International Conference on Software Maintenance (ICSM 1994), pp. 243–252, Washington, DC. IEEE Computer Society (1994)8. Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712–717. Springer, Heidelberg (2012) CrossRef9.Lahiri, S.K., Vaswani, K., Hoare, C.A.R.: Differential static analysis: opportunities, applications, and challenges. In: Proceedings of the FSE/SDP Workshop on Future of Software Engineering Research (FoSER 2010), pp. 201–204, ACM. New York (2010)10.Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef11.The Coq development team: The Coq proof assistant reference manual. LogiCal Project. Version 8.0 (2004)12. Partush, N., Yahav, E.: Abstract semantic differencing for numerical programs. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 238–258. Springer, Heidelberg (2013) CrossRef13.Partush, N., Yahav, E.: Abstract semantic differencing via speculative correlation. In: ACM International Conference on Object Oriented Programming Systems Languages and Applications(OOPSLA 2014), pp. 811–828, ACM. New York (2014)14.Person, S., Dwyer, M.B., Elbaum, S., Pǎsǎreanu, C.S.: Differential symbolic execution. In: 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering(SIGSOFT 2008/FSE-16), pp. 226–237, ACM (2008)15. Strichman, O., Godlin, B.: Regression verification - a practical way to verify programs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 496–501. Springer, Heidelberg (2008) CrossRef16.Yang, G., Person, S., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. ACM Trans. Softw. Eng. Methodol. 24(1), 3:1–3:42 (2014)CrossRef About this Chapter Title A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences Book Title Automated Technology for Verification and Analysis Book Subtitle 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings Pages pp 64-79 Copyright 2015 DOI 10.1007/978-3-319-24953-7_6 Print ISBN 978-3-319-24952-0 Online ISBN 978-3-319-24953-7 Series Title Lecture Notes in Computer Science Series Volume 9364 Series ISSN 0302-9743 Publisher Springer International Publishing Copyright Holder Springer International Publishing Switzerland Additional Links About this Book Topics Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence (incl. Robotics) Programming Techniques Industry Sectors Pharma Automotive Biotechnology Electronics IT & Software Telecommunications Aerospace Oil, Gas & Geosciences Engineering eBook Packages Computer Science Editors Bernd Finkbeiner (13) Geguang Pu (14) Lijun Zhang (15) Editor Affiliations 13. Universität des Saarlandes 14. East China Normal University 15. Chinese Academy of Sciences Authors Thibaut Girka (16) (17) David Mentré (16) Yann Régis-Gianas (17) Author Affiliations 16. Mitsubishi Electric R&D Centre Europe, 35708, Rennes, France 17. University of Paris Diderot, Sorbonne Paris Cité, PPS, UMR 7126 CNRS, PiR2, INRIA Paris-Rocquencourt, 75205, Paris, France Continue reading... To view the rest of this content please follow the download PDF link above.