research-article

SymTuner: maximizing the power of symbolic execution by adaptively tuning external parameters

Authors:

Hakjoo OhAuthors Info & Claims

ICSE '22: Proceedings of the 44th International Conference on Software Engineering

Pages 2068 - 2079

https://doi.org/10.1145/3510003.3510185

Published: 05 July 2022 Publication History

Abstract

We present SymTuner, a novel technique to automatically tune external parameters of symbolic execution. Practical symbolic execution tools have important external parameters (e.g., symbolic arguments, seed input) that critically affect their performance. Due to the huge parameter space, however, manually customizing those parameters is notoriously difficult even for experts. As a consequence, symbolic execution tools have typically been used in a suboptimal manner that, for example, simply relies on the default parameter settings of the tools and loses the opportunity for better performance. In this paper, we aim to change this situation by automatically configuring symbolic execution parameters. With SymTuner that takes parameter spaces to be tuned, symbolic executors are run without manual parameter configurations; instead, appropriate parameter values are learned and adjusted during symbolic execution. To achieve this, we present a learning algorithm that observes the behavior of symbolic execution and accordingly updates the sampling probability of each parameter space. We evaluated SymTuner with KLEE on 12 open-source C programs. The results show that SymTuner increases branch coverage of KLEE by 56% on average and finds 8 more bugs than KLEE with its default parameters over the latest releases of the programs.

References

[1]

Wasif Afzal, Richard Torkar, and Robert Feldt. 2009. A systematic review of search-based testing for non-functional system properties. Information and Software Technology (2009), 957--976.

[2]

J. Ansel, S. Kamil, K. Veeramachaneni, J. Ragan-Kelley, J. Bosboom, U. O'Reilly, and S. Amarasinghe. 2014. OpenTuner: An extensible framework for program autotuning. In 2014 23rd International Conference on Parallel Architecture and Compilation Techniques (PACT'14). 303--315.

[3]

Andrea Arcuri and Gordon Fraser. 2013. Parameter tuning or default values? An empirical investigation in search-based software engineering. Empirical Software Engineering (2013), 594--623.

[4]

Andrea Arcuri and Xin Yao. 2008. Search based software testing of object-oriented containers. Information Sciences (2008), 3075--3095.

[5]

Roberto Baldoni, Emilio Coppa, Daniele Cono D'elia, Camil Demetrescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques. ACM Comput. Surv. 51, 3, Article 50 (May 2018), 39 pages.

Digital Library

[6]

Peter Boonstoppel, Cristian Cadar, and Dawson Engler. 2008. RWset: Attacking path explosion in constraint-based test generation. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '08). 351--366.

Digital Library

[7]

Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. 1975. SELECT-a Formal System for Testing and Debugging Programs by Symbolic Execution. SIGPLAN Not. (1975), 234--245.

[8]

Xiangping Bu, Jia Rao, and Cheng-Zhong Xu. 2009. A Reinforcement Learning Approach to Online Web Systems Auto-Configuration. In Proceedings of the 2009 29th IEEE International Conference on Distributed Computing Systems (ICDCS '09). 2--11.

Digital Library

[9]

Suhabe Bugrara and Dawson Engler. 2013. Redundant State Detection for Dynamic Symbolic Execution. In Proceedings of the 2013 USENIX Conference on Annual Technical Conference (USENIX ATC'13). 199--212.

[10]

Jacob Burnim and Koushik Sen. 2008. Heuristics for Scalable Dynamic Test Generation. In Proceedings of 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE '08). 443--446.

Digital Library

[11]

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). 209--224.

Digital Library

[12]

C. Cadar, P. Godefroid, S. Khurshid, C. S. Pasareanu, K. Sen, N. Tillmann, and W. Visser. 2011. Symbolic execution for software testing in practice: preliminary assessment. In 2011 33rd International Conference on Software Engineering (ICSE). 1066--1071.

[13]

Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. Commun. ACM 56, 2 (2013), 82--90.

Digital Library

[14]

Sooyoung Cha, Seongjoon Hong, Junhee Lee, and Hakjoo Oh. 2018. Automatically Generating Search Heuristics for Concolic Testing. In Proceedings of the 40th International Conference on Software Engineering (ICSE '18). 1244--1254.

Digital Library

[15]

Sooyoung Cha, Seonho Lee, and Hakjoo Oh. 2018. Template-guided Concolic Testing via Online Learning. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE '18). 408--418.

Digital Library

[16]

Sooyoung Cha and Hakjoo Oh. 2019. Concolic Testing with Adaptively Changing Search Heuristics. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE '19). 235--245.

Digital Library

[17]

Sooyoung Cha and Hakjoo Oh. 2020. Making Symbolic Execution Promising by Learning Aggressive State-Pruning Strategy. In The 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE '20).

Digital Library

[18]

Junjie Chen, Wenxiang Hu, Lingming Zhang, Dan Hao, Sarfraz Khurshid, and Lu Zhang. 2018. Learning to accelerate symbolic execution via code transformation. In 32nd European Conference on Object-Oriented Programming (ECOOP '18).

[19]

Yaohui Chen, Peng Li, Jun Xu, Shengjian Guo, Rundong Zhou, Yulong Zhang, Tao Wei, and Long Lu. 2020. SAVIOR: Towards Bug-Driven Hybrid Testing. In 2020 IEEE Symposium on Security and Privacy (S&P '20). 1580--1596.

[20]

Dazhao Cheng, Jia Rao, Yanfei Guo, and Xiaobo Zhou. 2014. Improving MapReduce Performance in Heterogeneous Environments with Adaptive Task Tuning. In Proceedings of the 15th International Middleware Conference (Middleware '14). 97--108.

Digital Library

[21]

CREST. A concolic test generation tool for C. 2008. https://github.com/jburnim/crest.

[22]

Songyun Duan, Vamsidhar Thummala, and Shivnath Babu. 2009. Tuning Database Configuration Parameters with ITuned. Proc. VLDB Endow. (2009), 1246--1257.

Digital Library

[23]

Oscar Soria Dustmann, Klaus Wehrle, and Cristian Cadar. 2018. PARTI: A Multi-Interval Theory Solver for Symbolic Execution. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE '18). 430--440.

Digital Library

[24]

Gordon Fraser and Andrea Arcuri. 2011. EvoSuite: Automatic Test Suite Generation for Object-Oriented Software. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering (ESEC/FSE '11). 416--419.

Digital Library

[25]

Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed Automated Random Testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '05). 213--223.

Digital Library

[26]

Alex Groce, Chaoqiang Zhang, Eric Eide, Yang Chen, and John Regehr. 2012. Swarm Testing. In Proceedings of the 2012 International Symposium on Software Testing and Analysis (ISSTA '12). 78--88.

[27]

Mark Harman, Yue Jia, and Yuanyuan Zhang. 2015. Achievements, open problems and challenges for search based software testing. In 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST '15). 1--12.

[28]

Mark Harman and Bryan F Jones. 2001. Search-based software engineering. Information and software Technology (2001), 833--839.

[29]

Mark Harman, S Afshin Mansouri, and Yuanyuan Zhang. 2012. Search-based software engineering: Trends, techniques and applications. ACM Computing Surveys (CSUR) (2012), 1--61.

[30]

Mark Harman, Phil McMinn, Jerffeson Teixeira De Souza, and Shin Yoo. 2010. Search based software engineering: Techniques, taxonomy, tutorial. In Empirical software engineering and verification. 1--59.

[31]

Gerard J. Holzmann, Rajeev Joshi, and Alex Groce. 2011. Swarm Verification Techniques. IEEE Transactions on Software Engineering (2011), 845--857.

Digital Library

[32]

W. E. Howden. 1977. Symbolic Testing and the DISSECT Symbolic Evaluation System. IEEE Transactions on Software Engineering (1977), 266--278.

Digital Library

[33]

Frank Hutter, Holger H Hoos, Kevin Leyton-Brown, and Thomas Stützle. 2009. ParamILS: an automatic algorithm configuration framework. Journal of Artificial Intelligence Research (2009), 267--306.

[34]

Joxan Jaffar, Vijayaraghavan Murali, and Jorge A. Navas. 2013. Boosting Concolic Testing via Interpolation. In Proceedings of the 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE '13). 48--58.

[35]

Xiangyang Jia, Carlo Ghezzi, and Shi Ying. 2015. Enhancing Reuse of Constraint Solutions to Improve Symbolic Execution. In Proceedings of the 2015 International Symposium on Software Testing and Analysis (ISSTA '15). 177--187.

Digital Library

[36]

Yue Jia, Myra B. Cohen, Mark Harman, and Justyna Petke. 2015. Learning Combinatorial Interaction Test Generation Strategies Using Hyperheuristic Search. In Proceedings of the 37th International Conference on Software Engineering - Volume 1 (ICSE '15). 540--550.

Digital Library

[37]

Timotej Kapus, Frank Busse, and Cristian Cadar. 2020. Pending Constraints in Symbolic Execution for Better Exploration and Seeding. In Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering (ASE '20). 115--126.

Digital Library

[38]

Timotej Kapus and Cristian Cadar. 2019. A Segmented Memory Model for Symbolic Execution. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (Tallinn, Estonia) (ESEC/FSE 2019). Association for Computing Machinery, New York, NY, USA, 774--784.

Digital Library

[39]

Timotej Kapus, Martin Nowack, and Cristian Cadar. 2019. Constraints in Dynamic Symbolic Execution: Bitvectors or Integers?. In Tests and Proofs, Dirk Beyer and Chantal Keller (Eds.). Springer International Publishing, Cham, 41--54.

[40]

Richard M Karp. 1972. Reducibility among combinatorial problems. In Complexity of computer computations. 85--103.

[41]

James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 (1976), 385--394.

Digital Library

[42]

Yavuz Koroglu, Alper Sen, Ozlem Muslu, Yunus Mete, Ceyda Ulker, Tolga Tanriverdi, and Yunus Donmez. 2018. QBE: QLearning-based exploration of android applications. In 2018 IEEE 11th International Conference on Software Testing, Verification and Validation (ICST '18). 105--115.

[43]

Min Li, Liangzhao Zeng, Shicong Meng, Jian Tan, Li Zhang, Ali R. Butt, and Nicholas Fuller. 2014. MRONLINE: MapReduce Online Performance Tuning. In Proceedings of the 23rd International Symposium on High-Performance Parallel and Distributed Computing (HPDC '14). 165--176.

Digital Library

[44]

Xin Li, Yongjuan Liang, Hong Qian, Yi-Qi Hu, Lei Bu, Yang Yu, Xin Chen, and Xuandong Li. 2016. Symbolic Execution of Complex Program Driven by Machine Learning Based Constraint Solving. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE '16). 554--559.

Digital Library

[45]

You Li, Zhendong Su, Linzhang Wang, and Xuandong Li. 2013. Steering Symbolic Execution to Less Traveled Paths. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages, and Applications (OOPSLA '13). 19--32.

Digital Library

[46]

Phil McMinn. 2011. Search-based software testing: Past, present and future. In 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops. 153--163.

Digital Library

[47]

Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, and Abhik Roychoudhury. 2018. Symbolic Execution with Existential Second-Order Constraints. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE '18). 389--399.

Digital Library

[48]

M. Nowack. 2019. Fine-Grain Memory Object Representation in Symbolic Execution. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). 912--923.

[49]

OSDI'08_Coreutil_Experiments. 2008. https://klee.github.io/docs/coreutils-experiments.

[50]

Awanish Pandey, Phani Raj Goutham Kotcharlakota, and Subhajit Roy. 2019. Deferred Concretization in Symbolic Execution via Fuzzing. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '19). 228--238.

Digital Library

[51]

Corina S Păsăreanu and Neha Rungta. 2010. Symbolic PathFinder: symbolic execution of Java bytecode. In Proceedings of the IEEE/ACM international conference on Automated software engineering (ASE '10). 179--180.

Digital Library

[52]

David M. Perry, Andrea Mattavelli, Xiangyu Zhang, and Cristian Cadar. 2017. Accelerating Array Constraints in Symbolic Execution. In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '17). 68--78.

Digital Library

[53]

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 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE '05). 263--272.

[54]

Hyunmin Seo and Sunghun Kim. 2014. How We Get There: A Context-guided Search Strategy in Concolic Testing. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE '14). 413--424.

Digital Library

[55]

Shiqi Shen, Shweta Shinde, Soundarya Ramesh, Abhik Roychoudhury, and Prateek Saxena. 2019. Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints. In Proceedings of the Symposium on Network and Distributed System Security (NDSS '19).

[56]

Jiri Slaby, Jan Strejček, and Marek Trtík. 2013. Symbiotic: synergy of instrumentation, slicing, and symbolic execution. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '13). 630--632.

Digital Library

[57]

Helge Spieker, Arnaud Gotlieb, Dusica Marijan, and Morten Mossige. 2017. Reinforcement Learning for Automatic Test Case Prioritization and Selection in Continuous Integration. In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '17). 12--22.

Digital Library

[58]

Chameleon. A tool that performs concolic testing with adaptively changing search heuristics. 2019. https://github.com/kupl/chameleon.

[59]

Thomas Torsney-Weir, Ahmed Saad, Torsten Moller, Hans-Christian Hege, Britta Weber, Jean-Marc Verbavatz, and Steven Bergner. 2011. Tuner: Principled parameter finding for image segmentation algorithms using visual response surface exploration. IEEE Transactions on Visualization and Computer Graphics (2011), 1892--1901.

[60]

David Trabish, Andrea Mattavelli, Noam Rinetzky, and Cristian Cadar. 2018. Chopped Symbolic Execution. In Proceedings of the 40th International Conference on Software Engineering (ICSE '18). 350--360.

Digital Library

[61]

Dana Van Aken, Andrew Pavlo, Geoffrey J. Gordon, and Bohan Zhang. 2017. Automatic Database Management System Tuning Through Large-Scale Machine Learning. In Proceedings of the 2017 ACM International Conference on Management of Data (SIGMOD '17). 1009--1024.

Digital Library

[62]

Xinyu Wang, Jun Sun, Zhenbang Chen, Peixin Zhang, Jingyi Wang, and Yun Lin. 2018. Towards Optimal Concolic Testing. In Proceedings of the 40th International Conference on Software Engineering (ICSE '18). 291--302.

Digital Library

[63]

E. Wong, L. Zhang, S. Wang, T. Liu, and L. Tan. 2015. DASE: DocumentAssisted Symbolic Execution for Improving Automated Software Testing. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering (ICSE '15). 620--631.

[64]

Bowei Xi, Zhen Liu, Mukund Raghavachari, Cathy H. Xia, and Li Zhang. 2004. A Smart Hill-Climbing Algorithm for Application Server Configuration. In Proceedings of the 13th International Conference on World Wide Web (WWW '04). 287--296.

Digital Library

[65]

Guowei Yang, Corina S Păsăreanu, and Sarfraz Khurshid. 2012. Memoized symbolic execution. In Proceedings of the 2012 International Symposium on Software Testing and Analysis (ISSTA '12). 144--154.

Digital Library

[66]

Qiuping Yi, Zijiang Yang, Shengjian Guo, Chao Wang, Jian Liu, and Chen Zhao. 2018. Eliminating Path Redundancy via Postconditioned Symbolic Execution. IEEE Transactions on Software Engineering (2018), 25--43.

Digital Library

Cited By

Wang ZYang LChen MBu YLi ZWang QQin SYi XYin JFilkov VRay BZhou M(2024)Parf: Adaptive Parameter Refining for Abstract InterpretationProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695487(1082-1093)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695487
Tu HJiang LHong JDing XJiang H(2024)Concretely Mapped Symbolic Memory Locations for Memory Error DetectionIEEE Transactions on Software Engineering10.1109/TSE.2024.3395412(1-21)Online publication date: 2024
https://doi.org/10.1109/TSE.2024.3395412
Khan ZNamin A(2024)A Survey of Vulnerability Detection Techniques by Smart Contract ToolsIEEE Access10.1109/ACCESS.2024.340162312(70870-70910)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3401623

Recommendations

Revision of total hip arthroplasty: Clinical outcome of extended trochanteric osteotomy and intraoperative femoral fracture

In femoral revision arthroplasty the orthopaedic surgeon frequently has to decide between performing an extended trochanteric osteotomy or trying to remove the femoral stem without an osteotomy and taking the risk of an intraoperative fracture. As this ...
Biomechanical analyses of static and dynamic fixation techniques of retrograde interlocking femoral nailing using nonlinear finite element methods

Femoral shaft fractures can be treated using retrograde interlocking nailing systems; however, fracture nonunion still occurs. Dynamic fixation techniques, which remove either the proximal or distal locking screws, have been used to solve the problem of ...
Diagnostic value of bone scintigraphy for aseptic loosening after total knee arthroplasty

BACKGROUND: Despite technical improvements, aseptic loosening after total knee arthroplasty (TKA) remains a frequent complication. A one-stage revision arthroplasty is the most common therapeutic pathway.OBJECTIVE: The aim of this study was to evaluate ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '22: Proceedings of the 44th International Conference on Software Engineering

May 2022

2508 pages

ISBN:9781450392211

DOI:10.1145/3510003

General Chair:
Matthew B Dwyer
University of Virginia
,
Program Chairs:
Daniela Damian
University of Victoria, Canada
,
Andreas Zeller
CISPA, Germany

Copyright © 2022 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

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 July 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Qualifiers

Research-article

Funding Sources

National Research Foundation of Korea (NRF)

Conference

ICSE '22

Sponsor:

SIGSOFT

ICSE '22: 44th International Conference on Software Engineering

May 21 - 29, 2022

Pennsylvania, Pittsburgh

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
208
Total Downloads

Downloads (Last 12 months)67
Downloads (Last 6 weeks)4

Reflects downloads up to 27 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang ZYang LChen MBu YLi ZWang QQin SYi XYin JFilkov VRay BZhou M(2024)Parf: Adaptive Parameter Refining for Abstract InterpretationProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695487(1082-1093)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695487
Tu HJiang LHong JDing XJiang H(2024)Concretely Mapped Symbolic Memory Locations for Memory Error DetectionIEEE Transactions on Software Engineering10.1109/TSE.2024.3395412(1-21)Online publication date: 2024
https://doi.org/10.1109/TSE.2024.3395412
Khan ZNamin A(2024)A Survey of Vulnerability Detection Techniques by Smart Contract ToolsIEEE Access10.1109/ACCESS.2024.340162312(70870-70910)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3401623

View Options

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