research-article

Improving Coverage of Test Cases Generated by Symbolic PathFinder for Programs with Loops

Authors:

Rody Kersten,

Suzette Person,

Neha Rungta,

Oksana TkachukAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 40, Issue 1

Pages 1 - 5

https://doi.org/10.1145/2693208.2693243

Published: 06 February 2015 Publication History

Get Access

Abstract

Symbolic execution is a program analysis technique that is used for many purposes, one of which is test case generation. For loop-free programs, this generates a test set that achieves path coverage. Program loops, however, imply exponential growth of the number of paths in the best case and non-termination in the worst case. In practice, the number of loop unwindings needs to be bounded for analysis.

We consider symbolic execution in the context of the tool Symbolic Pathfinder. This tool extends the Java Pathfinder model-checker and relies on its bounded state-space exploration for termination. We present an implementation of k-bounded loop un- winding, which increases the amount of user-control over the symbolic execution of loops.

Bounded unwinding can be viewed as a naive way to prune paths through loops. When using symbolic execution for test case generation, branch coverage will likely be lost when paths are naively pruned. In order to improve coverage of branches within a loop body, we present a technique that semi-automatically concretizes variables used in a loop. The basic technique is limited and we therefore present annotations to manually steer symbolic execution towards certain branches, as well as ideas on how the technique can be extended to be more widely applicable.

References

[1]

J. Backes, S. Person, N. Rungta, and O. Tkachuk. Regression verification using impact summaries. In Model Checking Software, LNCS 7976, pages 99--116. Springer, 2013.

Google Scholar

[2]

C. Cadar, P. Godefroid, S. Khurshid, C. S. Păsăreanu, K. Sen, N. Tillmann, and W. Visser. Symbolic execution for software testing in practice: Preliminary assessment. In ICSE'11, pages 1066--1071. ACM, 2011.

Digital Library

Google Scholar

[3]

C. Gladisch. Verification-based test case generation for full feasible branch coverage. In SEFM '08, pages 159--168, Nov 2008.

Digital Library

Google Scholar

[4]

P. Godefroid and D. Luchaup. Automatic partial loop summarization in dynamic test generation. In ISSTA'11, pages 23--33. ACM, 2011.

Digital Library

Google Scholar

[5]

K. Havelund and T. Pressburger. Model checking java programs using Java Pathfinder. Int. Journal on Softw. Tools for Tech. Transfer, 2(4):366--381, 2000.

Crossref

Google Scholar

[6]

E. Mercer, S. Person, and N. Rungta. Computing and visualizing the impact of change with Java PathFinder extensions. SIGSOFT Softw. Eng. Notes, 37(6):1--5, Nov 2012.

Digital Library

Google Scholar

[7]

S. Person, M. B. Dwyer, S. Elbaum, and C. S. Păsăreanu. Differential symbolic execution. In FSE '08, pages 226--237. ACM, 2008.

Digital Library

Google Scholar

[8]

C. S. Păsăreanu and N. Rungta. Symbolic PathFinder: Symbolic execution of Java bytecode. In ASE '10, pages 179--180. ACM, 2010.

Digital Library

Google Scholar

[9]

C. S. Păsăreanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In Model Checking Software, LNCS 2989, pages 164--181. Springer, 2004.

Google Scholar

[10]

N. Rungta, S. Person, and J. Branchaud. A change impact analysis to characterize evolving program behaviors. In ICSM '12, pages 109--118, Sept 2012.

Digital Library

Google Scholar

[11]

P. Saxena, P. Poosankam, S. McCamant, and D. Song. Loop-extended symbolic execution on binary programs. In ISSTA '09, pages 225--236. ACM, 2009.

Digital Library

Google Scholar

[12]

M. Trtík. Symbolic Execution and Program Loops. PhD thesis, Faculty of Informatics, Masaryk University, 2013.

Google Scholar

[13]

X. Xiao, S. Li, T. Xie, and N. Tillmann. Characteristic studies of loop problems for structural test generation via symbolic execution. In ASE '13, pages 246--256, 2013.

Digital Library

Google Scholar

Cited By

View all

Nguena Timo OLangelier G(2019)Test Data Generation for Cyclic Executives with CBMC and Frama-CElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2016.01.004320:C(35-51)Online publication date: 5-Jan-2019
https://dl.acm.org/doi/10.1016/j.entcs.2016.01.004
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
Byun TSharma VRayadurgam SMcCamant SHeimdahl M(2017)Toward Rigorous Object-Code Coverage Criteria2017 IEEE 28th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE.2017.33(328-338)Online publication date: Oct-2017
https://doi.org/10.1109/ISSRE.2017.33

Index Terms

Improving Coverage of Test Cases Generated by Symbolic PathFinder for Programs with Loops
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Symbolic Path-Guided Test Cases for Models with Data and Time
Formal Aspects of Component Software
Abstract
This paper focuses on generating test cases from timed symbolic transition systems. At the heart of the generation process are symbolic execution techniques on data and time. Test cases look like finite symbolic trees with verdicts on their leaves ...
Improving function coverage with munch: a hybrid fuzzing and directed symbolic execution approach
SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing

Fuzzing and symbolic execution are popular techniques for finding vulnerabilities and generating test-cases for programs. Fuzzing, a blackbox method that mutates seed input values, is generally incapable of generating diverse inputs that exercise all ...
Improving Structural Testing of Object-Oriented Programs via Integrating Evolutionary Testing and Symbolic Execution
ASE '08: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering

Achieving high structural coverage such as branch coverage in object-oriented programs is an important and yet challenging goal due to two main challenges. First, some branches involve complex program logics and generating tests to cover them requires ...

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 40, Issue 1

January 2015

237 pages

ISSN:0163-5948

DOI:10.1145/2693208

Editor:
Michael Wing

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 February 2015

Published in SIGSOFT Volume 40, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
154
Total Downloads

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

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Nguena Timo OLangelier G(2019)Test Data Generation for Cyclic Executives with CBMC and Frama-CElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2016.01.004320:C(35-51)Online publication date: 5-Jan-2019
https://dl.acm.org/doi/10.1016/j.entcs.2016.01.004
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
Byun TSharma VRayadurgam SMcCamant SHeimdahl M(2017)Toward Rigorous Object-Code Coverage Criteria2017 IEEE 28th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE.2017.33(328-338)Online publication date: Oct-2017
https://doi.org/10.1109/ISSRE.2017.33

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

Symbolic Path-Guided Test Cases for Models with Data and Time

Improving function coverage with munch: a hybrid fuzzing and directed symbolic execution approach

Improving Structural Testing of Object-Oriented Programs via Integrating Evolutionary Testing and Symbolic Execution