research-article

Scaling Up Symbolic Analysis by Removing Z-Equivalent States

Authors:

Yepang LiuAuthors Info & Claims

ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 23, Issue 4

Article No.: 34, Pages 1 - 32

https://doi.org/10.1145/2652484

Published: 05 September 2014 Publication History

Abstract

Path explosion is a major issue in applying path-sensitive symbolic analysis to large programs. We observe that many symbolic states generated by the symbolic analysis of a procedure are indistinguishable to its callers. It is, therefore, possible to keep only one state from each set of equivalent symbolic states without affecting the analysis result. Based on this observation, we propose an equivalence relation called z-equivalence, which is weaker than logical equivalence, to relate a large number of z-equivalent states. We prove that z-equivalence is strong enough to guarantee that paths to be traversed by the symbolic analysis of two z-equivalent states are identical, giving the same solutions to satisfiability and validity queries. We propose a sound linear algorithm to detect z-equivalence. Our experiments show that the symbolic analysis that leverages z-equivalence is able to achieve more than ten orders of magnitude reduction in terms of search space. The reduction significantly alleviates the path explosion problem, enabling us to apply symbolic analysis in large programs such as Hadoop and Linux Kernel.

References

[1]

Saswat Anand, Corina S. Pǎsǎreanu, and Willem Visser. 2009. Symbolic execution with abstraction. Int. J. Softw. Tools Technol. Transf. 11, 1 (2009), 53--67. DOI=10.1007/s10009-008-0090-1 http://dx. doi.org/10.1007/s10009-008-0090-1

Digital Library

[2]

Domagoj Babic and Alan J. Hu. 2008. Calysto: Scalable and precise extended static checking. In Proceedings of the 30th International Conference on Software Engineering (ICSE'08). ACM, New York, NY, 211--220.

Digital Library

[3]

Domagoj Babic and Alan J. Hu. 2007. Structural abstraction of software verification conditions. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). Springer, Berlin. 371--383.

Digital Library

[4]

Peter Boonstoppel, Cristian Cadar, and Dawson Engler. 2008. RWset: Attacking path explosion in constraint-based test generation. In Proceedings of the European Joint Conference on Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08/ETAPS'08). C. R. Ramakrishnan and Jakob Rehof (Eds.), Springer-Verlag, Berlin, Heidelberg, 351--366.

Digital Library

[5]

Suhabe Bugrara and Dawson Engler. 2013. Redundant state detection for dynamic symbolic execution. In Proceedings of the USENIX Annual Technical Conference (ATC'13). USENIX Association, Berkeley, CA, 199--212.

Digital Library

[6]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08). USENIX Association, Berkeley, CA, 209--224.

Digital Library

[7]

Satish Chandra, Stephen J. Fink, and Manu Sridharan. 2009. SnuggleBug: A powerful approach to weakest preconditions. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'09). ACM, New York, NY, 363--374.

Digital Library

[8]

Avik Chaudhuri and Jeffrey S. Foster. 2010. Symbolic security analysis of Ruby-on-Rails Web applications. In Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS'10). ACM, New York, NY, 585--594.

Digital Library

[9]

Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2012. The S2E platform: Design, implementation, and applications. ACM Trans. Comput. Syst. 30, 1, Article 2 (2012).

Digital Library

[10]

L. A. Clarke. 1976. A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2, 3 (1976), 215--222.

Digital Library

[11]

Edmund Clarke, Daniel Kroening, and Karen Yorav. 2003. Behavioral consistency of C and verilog programs using bounded model checking. In Proceedings of the 40th Annual Design Automation Conference (DAC'03). ACM, New York, NY, 368--371.

Digital Library

[12]

Heming Cui, Gang Hu, Jingyue Wu, and Junfeng Yang. 2013. Verifying systems rules using rule-directed symbolic execution. In Proceedings of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'13). ACM, New York, NY, 329--342.

Digital Library

[13]

Isil Dillig, Thomas Dillig, and Alex Aiken. 2008. Sound, complete and scalable path-sensitive analysis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08). ACM, New York, NY, 270--280.

Digital Library

[14]

Vijay Ganesh and David L. Dill. 2007. A decision procedure for bit-vectors and arrays. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). Werner Damm and Holger Hermanns (Eds.), Springer-Verlag, Berlin, Heidelberg, 519--531.

Digital Library

[15]

Patrice Godefroid. 2007. Compositional dynamic test generation. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07). ACM, New York, NY, 47--54.

Digital Library

[16]

Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed automated random testing. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'05). ACM, New York, NY, 213--223.

Digital Library

[17]

Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. 2008. Program analysis as constraint solving. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08). ACM, New York, NY, 281--292.

Digital Library

[18]

Brian Hackett and Alex Aiken. 2006. How is aliasing used in systems software&quest; In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'06). ACM, New York, NY, 69--80.

Digital Library

[19]

Michael Huth and Mark Ryan. 2004. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.

Digital Library

[20]

James C. King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (1976), 385--394.

Digital Library

[21]

Sarfraz Khurshid, Corina S. Pǎsǎreanu, and Willem Visser. 2003. Generalized symbolic execution for model checking and testing. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03). Hubert Garavel and John Hatcliff (Eds.), Springer-Verlag, Berlin, Heidelberg, 553--568.

Digital Library

[22]

Nupur Kothari, Todd Millstein, and Ramesh Govindan. 2008. Deriving state machines from TinyOS programs using symbolic execution. In Proceedings of the 7th International Conference on Information Processing in Sensor Networks (IPSN'08). IEEE Computer Society, Los Alamitos, CA, 271--282.

Digital Library

[23]

Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea. 2012. Efficient state merging in symbolic execution. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'12). ACM, New York, NY, 193--204.

Digital Library

[24]

Yueqi Li, S. C. Cheung, Xiangxu Zhang, and Yepang Liu. 2013. Scaling up symbolic analysis by removing Beta-equivalent states. Technical Report HKUST-CS13-06. Hong Kong University of Science and Technology.

[25]

T. Murata. Petri nets: Properties, analysis and applications. 1989. Proc. IEEE, 77, 4, 541--580.

[26]

Mayur Naik, Hongseok Yang, Ghila Castelnuovo, and Mooly Sagiv. 2012. Abstractions from tests. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12). ACM, New York, NY, 373--386.

Digital Library

[27]

Suzette Person, Matthew B. Dwyer, Sebastian Elbaum, and Corina S. Pǎsǎreanu. 2008. Differential symbolic execution. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'08). ACM, New York, NY, 226--237.

Digital Library

[28]

Suzette Person, Guowei Yang, Neha Rungta, and Sarfraz Khurshid. 2011. Directed incremental symbolic execution. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'11). ACM, New York, NY, 504--515.

Digital Library

[29]

Corina S. Pǎsǎreanu, Peter C. Mehlitz, David H. Bushnell, Karen Gundy-Burlet, Michael Lowry, Suzette Person, and Mark Pape. 2008. Combining unit-level symbolic execution and system-level concrete execution for testing nasa software. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA'08). ACM, New York, NY, 15--26.

Digital Library

[30]

Dawei Qi, William N. Sumner, Feng Qin, Mai Zheng, Xiangyu Zhang, and Abhik Roychoudhury. 2012. Modeling software execution environment. In Proceedings of the 19th Working Conference on Reverse Engineering (WCRE'12). IEEE Computer Society, Los Alamitos, CA, 415--424.

Digital Library

[31]

Edna E. Reiter and Matthew Johnson Clayton. 2013. Limits of Computation: An Introduction to the Undecidable and the Intractable. CRC Press

Digital Library

[32]

Stuart Russell and Peter Norvig. 2003. Inference in first order logic. In Artificial Intelligence, A Modern Approach, Prentice Hall.

[33]

Raul Santelices and Mary Jean Harrold. 2010. Exploiting program dependencies for scalable multiple-path symbolic execution. In Proceedings of the 19th International Symposium on Software Testing and Analysis (ISSTA'10). ACM, New York, NY, 195--206.

Digital Library

[34]

Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A concolic unit testing engine for C. In Proceedings of the 10th European Software Engineering Conference held jointly with the 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'05). ACM, New York, NY, 263--272.

Digital Library

[35]

Junaid Haroon Siddiqui and Sarfraz Khurshid. 2012. Scaling symbolic execution using ranged analysis. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12). ACM, New York, NY, 523--536.

Digital Library

[36]

Edward Tsang. 1993. Problem redunction by removing redundant constraints. In Foundations of Constraint Satisfaction, Computation in Cognitive Science Series, Academic Pr.

[37]

Willem Visser, Corina S. Pǎsǎreanu, and Radek Pelánek. 2006. Test input generation for Java containers using state matching. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA'06). ACM, New York, NY, 37--48.

Digital Library

[38]

Yichen Xie, Andy Chou, and Dawson Engler. 2003. ARCHER: Using symbolic, path-sensitive analysis to detect memory access errors. In Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'03). ACM, New York, NY, 327--336.

Digital Library

Cited By

Sabbaghi AKeyvanpour M(2020)A Systematic Review of Search Strategies in Dynamic Symbolic ExecutionComputer Standards & Interfaces10.1016/j.csi.2020.103444(103444)Online publication date: May-2020
https://doi.org/10.1016/j.csi.2020.103444
Xuan JMartinez MDeMarco FClement MMarcote SDurieux TLe Berre DMonperrus M(2019)NopolIEEE Transactions on Software Engineering10.1109/TSE.2016.256081143:1(34-55)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.1109/TSE.2016.2560811
Sabbaghi ARashidy Kanan HKeyvanpour M(2019)FSCT: A new fuzzy search strategy in concolic testingInformation and Software Technology10.1016/j.infsof.2018.11.006107(137-158)Online publication date: Mar-2019
https://doi.org/10.1016/j.infsof.2018.11.006
Show More Cited By

Index Terms

Scaling Up Symbolic Analysis by Removing Z-Equivalent States

Recommendations

Symbolic and semisymbolic analysis of electronic circuit in maple
CSS'11: Proceedings of the 5th WSEAS international conference on Circuits, systems and signals

This paper presents a usage of Maple program for electric and electronic circuit analysis. The special package PraCAn has been used for this purpose. This contribution introduces possibilities of the package for circuit linearization and following ac ...
Universally Composable Symbolic Security Analysis

In light of the growing complexity of cryptographic protocols and applications, it becomes highly desirable to mechanize—and eventually automate—the security analysis of protocols. A natural step towards automation is to allow for symbolic security ...
Symbolic state validation through runtime data
ASE '14: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering

Real world programs are typically built on top of many library functions. Symbolic analysis of these programs generally requires precise models of these functions? Application Programming Interfaces (APIs), which are mostly unavailable because these ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology

ACM Transactions on Software Engineering and Methodology Volume 23, Issue 4

Special Issue International Conference on Software Engineering (ICSE 2012) and Regular Papers

August 2014

232 pages

ISSN:1049-331X

EISSN:1557-7392

DOI:10.1145/2668018

Editors:
David S. Rosenblum
National University of Singapore, Singapore
,
Gail C. Murphy,
Mauro Pezzé

Issue’s Table of Contents

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2014

Accepted: 01 March 2014

Revised: 01 February 2014

Received: 01 July 2013

Published in TOSEM Volume 23, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
376
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)3

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sabbaghi AKeyvanpour M(2020)A Systematic Review of Search Strategies in Dynamic Symbolic ExecutionComputer Standards & Interfaces10.1016/j.csi.2020.103444(103444)Online publication date: May-2020
https://doi.org/10.1016/j.csi.2020.103444
Xuan JMartinez MDeMarco FClement MMarcote SDurieux TLe Berre DMonperrus M(2019)NopolIEEE Transactions on Software Engineering10.1109/TSE.2016.256081143:1(34-55)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.1109/TSE.2016.2560811
Sabbaghi ARashidy Kanan HKeyvanpour M(2019)FSCT: A new fuzzy search strategy in concolic testingInformation and Software Technology10.1016/j.infsof.2018.11.006107(137-158)Online publication date: Mar-2019
https://doi.org/10.1016/j.infsof.2018.11.006
Yang GFilieri ABorges MClun DWen J(2018)Advances in Symbolic Execution10.1016/bs.adcom.2018.10.002Online publication date: 2018
https://doi.org/10.1016/bs.adcom.2018.10.002
Li YCheung SCrnkovic IChechik MGrünbacher P(2014)Symbolic state validation through runtime dataProceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering10.1145/2642937.2642973(187-198)Online publication date: 15-Sep-2014
https://dl.acm.org/doi/10.1145/2642937.2642973

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents