demonstration

Symbolic PathFinder: symbolic execution of Java bytecode

Authors:

Corina S. Păsăreanu,

Neha RungtaAuthors Info & Claims

ASE '10: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering

Pages 179 - 180

https://doi.org/10.1145/1858996.1859035

Published: 20 September 2010 Publication History

Get Access

Abstract

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 representing multiple concrete inputs. Values of variables are represented as constraints generated from the analysis of Java bytecode. The constraints are solved using off-the shelf solvers to generate test inputs guaranteed to achieve complex coverage criteria. SPF has been used successfully at NASA, in academia, and in industry.

References

[1]

}}S. Anand, C. Păsăreanu, and W. Visser. JPF-SE: A Symbolic Execution Extension to Java PathFinder. TACAS, pages 134--138, 2007.

Digital Library

Google Scholar

[2]

}}X. Deng, J. Lee, and Robby. Bogor/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In ASE, 2006.

Digital Library

Google Scholar

[3]

}}P. Godefroid, N. Klarlund, and K. Sen. Dart: directed automated random testing. SIGPLAN Not., 40(6):213--223, 2005.

Digital Library

Google Scholar

[4]

}}Java PathFinder Tool-set. http://babelfish.arc.nasa.gov/trac/jpf.

Google Scholar

[5]

}}S. Khurshid, C. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. Proc. TACAS, pages 553--568, 2003.

Digital Library

Google Scholar

[6]

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

Digital Library

Google Scholar

[7]

}}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 Proc. ISSTA, 2008.

Digital Library

Google Scholar

[8]

}}N. Rungta, E. G. Mercer, and W. Visser. Efficient testing of concurrent programs with abstraction-guided symbolic execution. SPIN, 2009.

Digital Library

Google Scholar

[9]

}}K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for C. In Proc. ESEC/FSE-13, pages 263--272, New York, NY, USA, 2005. ACM.

Digital Library

Google Scholar

[10]

}}M. Staats and C. Pasareanu. Parallel Symbolic Execution for Structural Test Generation. In ISSTA. ACM, 2010.

Digital Library

Google Scholar

Cited By

View all

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
Yi QYu YYang G(2024)Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug FindingProceedings of the ACM on Programming Languages10.1145/36564438:PLDI(1633-1655)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656443
Hu GWang ZTang CShen JDong ZYao SChen H(2024)WeBridge: Synthesizing Stored Procedures for Large-Scale Real-World Web ApplicationsProceedings of the ACM on Management of Data10.1145/36393192:1(1-29)Online publication date: 26-Mar-2024
https://dl.acm.org/doi/10.1145/3639319
Show More Cited By

Index Terms

Symbolic PathFinder: symbolic execution of Java bytecode

Recommendations

Symbolic Arrays in Symbolic PathFinder

Symbolic Execution is a program analysis technique used to increase software reliability. Modern software often manipulate complex data structures, many of which being similar to arrays. We present a novel approach and implementation in Symbolic ...
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 ...
Shadow Symbolic Execution with Java PathFinder

Regression testing ensures that a software system when it evolves still performs correctly and that the changes introduce no unintended side-effects. However, the creation of regression test cases that show divergent behavior needs a lot of effort. A ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ASE '10: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering

September 2010

534 pages

ISBN:9781450301169

DOI:10.1145/1858996

General Chair:
Charles Pecheur
Université catholique de Louvain, Belgium
,
Program Chairs:
Jamie Andrews
University of Western Ontario, Canada
,
Elisabetta Di Nitto
Politecnico di Milano, Italy

Permission to make digital or hard copies of part or all 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 third-party components of this work must be honored. For all other uses, contact the Owner/Author.

In-Cooperation

IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 September 2010

Check for updates

Author Tags

Qualifiers

Demonstration

Conference

ASE10

Sponsor:

ASE10: IEEE/ACM International Conference on Automated Software Engineering

September 20 - 24, 2010

Antwerp, Belgium

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

185
Total Citations
View Citations
1,535
Total Downloads

Downloads (Last 12 months)73
Downloads (Last 6 weeks)15

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

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
Yi QYu YYang G(2024)Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug FindingProceedings of the ACM on Programming Languages10.1145/36564438:PLDI(1633-1655)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656443
Hu GWang ZTang CShen JDong ZYao SChen H(2024)WeBridge: Synthesizing Stored Procedures for Large-Scale Real-World Web ApplicationsProceedings of the ACM on Management of Data10.1145/36393192:1(1-29)Online publication date: 26-Mar-2024
https://dl.acm.org/doi/10.1145/3639319
Yang MLie DPapernot N(2024)Exploring Strategies for Guiding Symbolic Analysis with Machine Learning Prediction2024 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER60148.2024.00073(659-669)Online publication date: 12-Mar-2024
https://doi.org/10.1109/SANER60148.2024.00073
Zhang YWang LWang ZShangguan D(2024)Exploring Use of Symbolic Execution for Service Analysis2024 54th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume (DSN-S)10.1109/DSN-S60304.2024.00014(12-16)Online publication date: 24-Jun-2024
https://doi.org/10.1109/DSN-S60304.2024.00014
Glock JPichler JPinzger M(2024)PASDAJournal of Systems and Software10.1016/j.jss.2024.112037213:COnline publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1016/j.jss.2024.112037
Liu XYu PMa X(2024)An Empirical Study on Automated Test Generation Tools for Java: Effectiveness and ChallengesJournal of Computer Science and Technology10.1007/s11390-023-1935-539:3(715-736)Online publication date: 1-May-2024
https://dl.acm.org/doi/10.1007/s11390-023-1935-5
Zhang GShuai ZMa KLiu KChen ZWang J(2024)FDSE: Enhance Symbolic Execution by Fuzzing-based Pre-Analysis (Competition Contribution)Fundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_16(304-308)Online publication date: 6-Apr-2024
https://doi.org/10.1007/978-3-031-57259-3_16
Artho CParízek PQu DGalgali VYi P(2024)JPF: From 2003 to 2023Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_1(3-22)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57249-4_1
Mallissery SWu Y(2023)Demystify the Fuzzing Methods: A Comprehensive SurveyACM Computing Surveys10.1145/362337556:3(1-38)Online publication date: 5-Oct-2023
https://dl.acm.org/doi/10.1145/3623375
Show More Cited By

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 Arrays in Symbolic PathFinder

Abstract pathfinder

Shadow Symbolic Execution with Java PathFinder