Article

Test input generation with java PathFinder

Authors:

Corina S. Pǎsǎreanu,

Sarfraz KhurshidAuthors Info & Claims

ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis

Pages 97 - 107

https://doi.org/10.1145/1007512.1007526

Published: 01 July 2004 Publication History

Abstract

We show how model checking and symbolic execution can be used to generate test inputs to achieve structural coverage of code that manipulates complex data structures. We focus on obtaining branch-coverage during unit testing of some of the core methods of the red-black tree implementation in the Java TreeMap library, using the Java PathFinder model checker. Three different test generation techniques will be introduced and compared, namely, straight model checking of the code, model checking used in a black-box fashion to generate all inputs up to a fixed size, and lastly, model checking used during white-box test input generation. The main contribution of this work is to show how efficient white-box test input generation can be done for code manipulating complex data, taking into account complex method preconditions.

References

[1]

The economic impacts of inadequate infrastructure for software testing. National Institute of Standards and Technology, Planning report 02-3, May 2002.

[2]

R. J. Adam J. Chlipala, Thomas A. Henzinger and R. Majumdar. Generating tests from counterexamples. In Proceedings of the 26th International Conference on Software Engineering (ICSE), Edinburgh, Scotland, May 2004.

Digital Library

[3]

P. Ammann and P. Black. A specification-based coverage metric to evaluate test sets. In Proceedings of the 4th IEEE International Symposium on High Assurance Systems and Engineering, 1999.

Digital Library

[4]

P. Ammann, P. E. Black, and W. Majurski. Using model checking to generate tests from specifications. In Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods, 1998.

Digital Library

[5]

C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu, and W. Visser. Experiments with test case generation and runtime analysis. In Proceedings of the 10th International Workshop on Abstract State Machines, Taormina, Italy, March 2003.

Digital Library

[6]

T. Ball. Abstraction-guided test generation: A case study, 2003. Microsoft Research Technical Report MSR-TR-2003-86.

[7]

T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In Proc. 8th International SPIN Workshop on Model Checking of Software, pages 103--122, 2001.

Digital Library

[8]

T. Ball and S. K. Rajamani. The SLAM project: Debugging system software via static analysis. In Proc. 29th Annual ACM Symposium on the Principles of Programming Languages (POPL), pages 1--3, 2002.

Digital Library

[9]

B. Beizer. Software Testing Techniques. International Thomson Computer Press, 1990.

Digital Library

[10]

C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates. In Proc. International Symposium on Software Testing and Analysis (ISSTA), pages 123--133, July 2002.

Digital Library

[11]

G. Brat, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, W. Visser, and R. Washington. Experimental evaluation of verification and validation tools on martian rover software. In Proceedings of the SEI/CM Software Model Checking Workshop, Pittsburgh, March 2003. To Appear in Formal Methods in System Design Journal.

Digital Library

[12]

J. Chang and D. J. Richardson. Structural specification-based testing: Automated support and experimental evaluation. In Proc. 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), pages 285--302, Sept. 1999.

Digital Library

[13]

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, MA, 1999.

Digital Library

[14]

L. A. Clarke. A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering, Sept. 1976.

Digital Library

[15]

J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proc. 22nd International Conference on Software Engineering (ICSE), June 2000.

Digital Library

[16]

T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, Cambridge, MA, 1990.

Digital Library

[17]

C. Demartini, R. Iosif, and R. Sisto. A deadlock detection tool for concurrent Java programs. Software - Practice and Experience, July 1999.

Digital Library

[18]

M. R. Donat. Automating formal specification based testing. In Proc. Conference on Theory and Practice of Software Development, volume 1214, pages 833--847, Lille, France, 1997.

Digital Library

[19]

R.-K. Doong and P. G. Frankl. The astoot approach to testing object-oriented programs. ACM Transactions on Software Engineering and Methodology (TOSEM), 3(2):101--130, 1994.

Digital Library

[20]

Foundations of Software Engineering, Microsoft Research. The AsmL test generator tool. http://research.microsoft.com/fse/asml/doc/AsmLTester.html.

[21]

A. Gargantini and C. Heitmeyer. Using model checking to generate tests from requirements specifications. In Proceedings of the 7th European engineering conference held jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE). Springer-Verlag, 1999.

Digital Library

[22]

P. Godefroid. Model checking for programming languages using VeriSoft. In Proceedings of the 24th Annual ACM Symposium on the Principles of Programming Languages (POPL), pages 174--186, Paris, France, Jan. 1997.

Digital Library

[23]

J. Goodenough and S. Gerhart. Toward a theory of test data selection. IEEE Transactions on Software Engineering, June 1975.

Digital Library

[24]

A. Gotlieb, B. Botella, and M. Rueher. Automatic test data generation using constraint solving techniques. In Proc. International Symposium on Software Testing and Analysis (ISSTA), Clearwater Beach, FL, 1998.

Digital Library

[25]

W. Grieskamp, Y. Gurevich, W. Schulte, and M. Veanes. Generating finite state machines from abstract state machines. In Proc. International Symposium on Software Testing and Analysis (ISSTA), pages 112--122, July 2002.

Digital Library

[26]

M. P. E. Heimdahl, S. Rayadurgam, W. Visser, D. George, and J. Gao. Auto-generating test sequences using model checkers: A case study. In Proc. 3rd International Workshop on Formal Approaches to Testing of Software (FATES), Montreal, Canada, Oct. 2003.

[27]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with blast. In Proceedings of the Tenth International SPIN Workshop on Model Checking of Software, volume 2648 of LNCS, 2003.

Digital Library

[28]

H. S. Hong, I. Lee, O. Sokolsky, and H. Ural. A temporal logic based theory of test coverage and generation. In Proc. 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Grenoble, France, April 2002.

Digital Library

[29]

J. C. Huang. An approach to program testing. ACM Computing Surveys, 7(3), 1975.

Digital Library

[30]

S. Khurshid, C. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proc. 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Warsaw, Poland, April 2003.

Digital Library

[31]

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

Digital Library

[32]

B. Korel. Automated test data generation for programs with procedures. San Diego, CA, 1996.

[33]

T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In Proc. Static Analysis Symposium, Santa Barbara, CA, June 2000.

Digital Library

[34]

D. Marinov. Testing Using a Solver for Imperative Constraints. PhD thesis, Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 2004. (to appear).

[35]

D. Marinov and S. Khurshid. TestEra: A novel framework for automated testing of Java programs. In Proc. 16th IEEE International Conference on Automated Software Engineering (ASE), San Diego, CA, Nov. 2001.

Digital Library

[36]

A. Moeller and M. I. Schwartzbach. The pointer assertion logic engine. In Proc. SIGPLAN Conference on Programming Languages Design and Implementation, Snowbird, UT, June 2001.

Digital Library

[37]

J. Offutt and A. Abdurazik. Generating tests from UML specifications. In Proc. Second International Conference on the Unified Modeling Language, Oct. 1999.

Digital Library

[38]

C. Pasareanu and W. Visser. Verification of java programs using symbolic execution and invariant generation. In Proceedings of the 11th International SPIN Workshop on Model Checking of Software, volume 2989 of LNCS. Springer-Verlag, 2004.

[39]

J. Penix, W. Visser, E. Engstrom, A. Larson, and N. Weininger. Verification of Time Partitioning in the DEOS Scheduler Kernel. In Proceedings of the 22nd International Conference on Software Engineering (ICSE), Limeric, Ireland., June 2000. ACM Press.

Digital Library

[40]

W. Pugh. The Omega test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 31(8), Aug. 1992.

Digital Library

[41]

C. V. Ramamoorthy, S.-B. F. Ho, and W. T. Chen. On the automated generation of program test data. IEEE Transactions on Software Engineering, 2(4), 1976.

Digital Library

[42]

M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Trans. Prog. Lang. Syst., Jan. 1998.

Digital Library

[43]

W. Visser, K. Havelund, G. Brat, S.-J. Park, and F. Lerda. Model Checking Programs . Automated Software Engineering Journal, 10(2), April 2003.

Digital Library

[44]

G. Yorsh, T. W. Reps, and S. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In Proceedings of the 10th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Barcelona, Spain, April 2004.

Cited By

Takashima YCho CMartins RJia LPăsăreanu C(2024)Crabtree: Rust API Test Synthesis Guided by Coverage and TypeProceedings of the ACM on Programming Languages10.1145/36897338:OOPSLA2(618-647)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689733
Wu YHumayun AGulzar MKim M(2024)Natural Symbolic Execution-Based Testing for Big Data AnalyticsProceedings of the ACM on Software Engineering10.1145/36608251:FSE(2677-2700)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660825
Barth MJakobs M(2024)Test-Case Generation with Automata-Based Software Model CheckingModel Checking Software10.1007/978-3-031-66149-5_14(248-267)Online publication date: 10-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-66149-5_14
Show More Cited By

Index Terms

Test input generation with java PathFinder

Recommendations

Test input generation with java PathFinder

We show how model checking and symbolic execution can be used to generate test inputs to achieve structural coverage of code that manipulates complex data structures. We focus on obtaining branch-coverage during unit testing of some of the core methods ...
Test input generation for red-black trees using abstraction
ASE '05: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering

We consider the problem of test input generation for code that manipulates complex data structures. Test inputs are sequences of method calls from the data structure interface. We describe test input generation techniques that rely on state matching to ...
Test input generation with Java PathFinder: then and now (invited talk abstract)
ISSTA 2018: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis

The paper Test Input Generation With Java PathFinder was published in the International Symposium on Software Testing and Analysis (ISSTA) 2004 Proceedings, and has now been selected to receive the ISSTA 2018 Retrospective Impact Paper Award. The paper ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis

July 2004

294 pages

ISBN:1581138202

DOI:10.1145/1007512

General Chair:
George Avrunin
University of Massachusetts, USA
,
Program Chair:
Gregg Rothermel
University of Nebraska -- Lincoln, USA

ACM SIGSOFT Software Engineering Notes Volume 29, Issue 4
July 2004
284 pages
ISSN:0163-5948
DOI:10.1145/1013886
Issue’s Table of Contents

Copyright © 2004 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ISSTA04

Sponsor:

ISSTA04: International Symposium on Software Testing and Analysis 2004

July 11 - 14, 2004

Massachusetts, Boston, USA

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

419
Total Citations
View Citations
2,773
Total Downloads

Downloads (Last 12 months)62
Downloads (Last 6 weeks)9

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Takashima YCho CMartins RJia LPăsăreanu C(2024)Crabtree: Rust API Test Synthesis Guided by Coverage and TypeProceedings of the ACM on Programming Languages10.1145/36897338:OOPSLA2(618-647)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689733
Wu YHumayun AGulzar MKim M(2024)Natural Symbolic Execution-Based Testing for Big Data AnalyticsProceedings of the ACM on Software Engineering10.1145/36608251:FSE(2677-2700)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660825
Barth MJakobs M(2024)Test-Case Generation with Automata-Based Software Model CheckingModel Checking Software10.1007/978-3-031-66149-5_14(248-267)Online publication date: 10-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-66149-5_14
Nilizadeh ALeavens GPăsăreanu CNoller Y(2023)JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-guided Fuzzing and Runtime Assertion CheckingFormal Aspects of Computing10.1145/360753836:1(1-24)Online publication date: 5-Aug-2023
https://dl.acm.org/doi/10.1145/3607538
Bouajjani AEnea CRomán-Calvo E(2023)Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation LevelsProceedings of the ACM on Programming Languages10.1145/35912437:PLDI(565-590)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591243
Costea ATiwari AChianasta SR KRoychoudhury ASergey I(2023)Hippodrome: Data Race Repair Using Static Analysis SummariesACM Transactions on Software Engineering and Methodology10.1145/354694232:2(1-33)Online publication date: 31-Mar-2023
https://dl.acm.org/doi/10.1145/3546942
Bousy IBarr EClark D(2023)PopArt: Ranked Testing EfficiencyIEEE Transactions on Software Engineering10.1109/TSE.2022.321479649:4(2221-2238)Online publication date: 1-Apr-2023
https://doi.org/10.1109/TSE.2022.3214796
Copia JMolina FAguirre NFrias MGorla APonzio P(2023)Precise Lazy Initialization for Programs with Complex Heap Inputs2023 IEEE 34th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE59848.2023.00080(752-762)Online publication date: 9-Oct-2023
https://doi.org/10.1109/ISSRE59848.2023.00080
Guo SWan XYou WLiang BShi WZhang YHuang JZhang JGrundy JPollock LPenta M(2023)Operand-Variation-Oriented Differential Analysis for Fuzzing Binding Calls in PDF ReadersProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00020(95-107)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE48619.2023.00020
Rahman SLi CShi AGrundy J(2023)TSVD4J: Thread-Safety Violation Detection for JavaProceedings of the 45th International Conference on Software Engineering: Companion Proceedings10.1109/ICSE-Companion58688.2023.00029(78-82)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE-Companion58688.2023.00029
Show More Cited By

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents