research-article

Towards a lazier symbolic pathfinder

Authors:

Benjamin Hillery,

Eric Mercer,

Neha Rungta,

Suzette PersonAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 39, Issue 1

Pages 1 - 5

https://doi.org/10.1145/2557833.2560579

Published: 11 February 2014 Publication History

Get Access

Abstract

To explore the state space of programs with complex user-defined data structures, most symbolic execution engines use the lazy initialization algorithm. Symbolic Pathfinder (SPF) is the symbolic execution engine for the Java PathFinder (JPF) model checker; SPF too contains an implementation of the lazy initialization algorithm. A number of extensions to the original lazy initialization algorithm have since been published. One such extension is the lazier# algorithm which demonstrated dramatic performance gains over the other algorithms. There is, however, no open-source implementation of the lazier# algorithm available. This work is an implementation of the the lazier# algorithm within the Symbolic PathFinder framework. In addition, this work describes the implementation of two heap bounding techniques in SPF, namely k-bounding and n-bounding. The purpose of this paper is to discuss the nature of the improvements, implementation details, usage and performance test results.

References

[1]

C. Cadar and D. R. Engler. Execution generated test cases: How to make systems code crash itself. In SPIN, pages 2--23, 2005.

Digital Library

Google Scholar

[2]

L. A. Clarke. A program testing system. In Proceedings of the 1976 annual conference, ACM '76, pages 488--491, 1976.

Digital Library

Google Scholar

[3]

X. Deng, J. Lee, and Robby. Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In ASE '06: Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, pages 157--166, Washington, DC, USA, 2006. IEEE Computer Society.

Digital Library

Google Scholar

[4]

X. Deng, J. Lee, and Robby. Efficient and formal generalized symbolic execution. Autom. Softw. Eng., 19(3):233--301, 2012.

Digital Library

Google Scholar

[5]

X. Deng, Robby, and J. Hatcliff. Towards a case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs. In SEFM '07: Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods, pages 273--282, Washington, DC, USA, 2007. IEEE Computer Society.

Digital Library

Google Scholar

[6]

J. Geldenhuys, N. Aguirre, M. F. Frias, and W. Visser. Bounded lazy initialization. In NASA Formal Methods, pages 229--243. Springer, 2013.

Google Scholar

[7]

P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In PLDI, pages 213--223, 2005.

Digital Library

Google Scholar

[8]

S. Khurshid, C. S. Păsăreanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS, pages 553--568, 2003.

Digital Library

Google Scholar

[9]

J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976.

Digital Library

Google Scholar

[10]

C. S. Păsăreanu and N. Rungta. Symbolic Pathfinder: symbolic execution of Java bytecode. In Proceedings of the IEEE/ACM international conference on Automated software engineering, pages 179--180. ACM, 2010.

Digital Library

Google Scholar

[11]

C. S. Păsăreanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In ISSTA, pages 15--25, 2008.

Digital Library

Google Scholar

[12]

K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for C. In ESEC/FSE, pages 263--272, 2005.

Digital Library

Google Scholar

[13]

M. A. Weiss. Data Structures and Algorithm Analysis in Java. Addison-Wesley, 1999.

Digital Library

Google Scholar

Cited By

View all

Hillery BMercer ERungta NPerson S(2016)Exact Heap Summaries for Symbolic ExecutionProceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 958310.1007/978-3-662-49122-5_10(206-225)Online publication date: 17-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-662-49122-5_10

Index Terms

Towards a lazier symbolic pathfinder

Recommendations

Abstract pathfinder

We present Abstract Pathfinder, an extension to the Java Pathfinder (JPF) verification tool-set that supports data abstraction to reduce the large data domains of a Java program to small, finite abstract domains, making the program more amenable to ...
Symbolic PathFinder: symbolic execution of Java bytecode
ASE '10: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering

Symbolic Pathfinder (SPF) combines symbolic execution with model checking and constraint solving for automated test case generation and error detection in Java programs with unspecified inputs. In this tool, programs are executed on symbolic inputs ...
Symbolic PathFinder v7

We describe Symbolic PathFinder v7 in terms of its updated design addressing the changes of Java PathFinder v7 and of its new optimization when computing path conditions. Furthermore, we describe the Symbolic Execution Tree Extension; a newly added ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 39, Issue 1

January 2014

193 pages

ISSN:0163-5948

DOI:10.1145/2557833

Editor:
Will Tracz
Lockheed Martin IS&GS, Endicott, NY

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 February 2014

Published in SIGSOFT Volume 39, Issue 1

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
78
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Hillery BMercer ERungta NPerson S(2016)Exact Heap Summaries for Symbolic ExecutionProceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 958310.1007/978-3-662-49122-5_10(206-225)Online publication date: 17-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-662-49122-5_10

View Options

Login options

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

Cited By

Index Terms

Recommendations

Abstract pathfinder

Symbolic PathFinder: symbolic execution of Java bytecode

Symbolic PathFinder v7