More Web Proxy on the site http://driver.im/

research-article

Conc-iSE: incremental symbolic execution of concurrent software

Authors:

Chao WangAuthors Info & Claims

ASE '16: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering

Pages 531 - 542

https://doi.org/10.1145/2970276.2970332

Published: 25 August 2016 Publication History

Abstract

Software updates often introduce new bugs to existing code bases. Prior regression testing tools focus mainly on test case selection and prioritization whereas symbolic execution tools only handle code changes in sequential software. In this paper, we propose the first incremental symbolic execution method for concurrent software to generate new tests by exploring only the executions affected by code changes between two program versions. Specifically, we develop an inter-thread and inter-procedural change-impact analysis to check if a statement is affected by the changes and then leverage the information to choose executions that need to be reexplored. We also check if execution summaries computed in the previous program can be used to avoid redundant explorations in the new program. We have implemented our method in an incremental symbolic execution tool called Conc-iSE and evaluated it on a large set of multithreaded C programs. Our experiments show that the new method can significantly reduce the overall symbolic execution time when compared with state-of-the-art symbolic execution tools such as KLEE.

References

[1]

J. D. Backes, S. Person, N. Rungta, and O. Tkachuk. Regression verification using impact summaries. In International SPIN Workshop on Model Checking Software, pages 99–116, 2013.

[2]

M. Bravenboer and Y. Smaragdakis. Strictly declarative specification of sophisticated points-to analyses. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications, pages 243–262, 2009.

Digital Library

[3]

C. Cadar, D. Dunbar, and D. R. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Symposium on Operating Systems Design and Implementation, pages 209–224, 2008.

Digital Library

[4]

D. Chu and J. Jaffar. A framework to synergize partial order reduction with state interpolation. In International Haifa Verification Conference, pages 171–187, 2014.

[5]

L. Ciortea, C. Zamfir, S. Bucur, V. Chipounov, and G. Candea. Cloud9: a software testing service. Operating Systems Review, 43(4):5–10, 2009.

Digital Library

[6]

E. Dijkstra. A Discipline of Programming. Prentice Hall, NJ, 1976.

Digital Library

[7]

A. Farzan, A. Holzer, N. Razavi, and H. Veith. Con2colic testing. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 37–47, 2013.

Digital Library

[8]

J. Ferrante, K. J. Ottenstein, and J. D. Warren. The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst., 9(3):319–349, July 1987.

Digital Library

[9]

C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 110–121, 2005.

Digital Library

[10]

M. K. Ganai, N. Arora, C. Wang, A. Gupta, and G. Balakrishnan. BEST: A symbolic testing tool for predicting multi-threaded program failures. In IEEE/ACM International Conference On Automated Software Engineering, pages 596–599, 2011.

Digital Library

[11]

P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. Springer, 1996.

Digital Library

[12]

S. Guo, M. Kusano, C. Wang, Z. Yang, and A. Gupta. Assertion guided symbolic execution of multithreaded programs. In ACM SIGSOFT Symposium on Foundations of Software Engineering, 2015.

Digital Library

[13]

K. Herzig, M. Greiler, J. Czerwonka, and B. Murphy. The art of testing less without sacrificing quality. In International Conference on Software Engineering, pages 483–493, Piscataway, NJ, USA, 2015. IEEE Press.

Digital Library

[14]

K. Hoder, N. Bjørner, and L. de Moura. muZ - an efficient engine for fixed points with constraints. In International Conference on Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pages 457–462, 2011.

Digital Library

[15]

S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst., 12(1):26–60, Jan. 1990.

Digital Library

[16]

J. Jaffar, V. Murali, and J. A. Navas. Boosting concolic testing via interpolation. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 48–58, 2013.

Digital Library

[17]

V. Jagannath, Q. Luo, and D. Marinov. Change-aware preemption prioritization. In International Symposium on Software Testing and Analysis, 2011.

Digital Library

[18]

V. Kahlon and C. Wang. Universal Causality Graphs: A precise happens-before model for detecting bugs in concurrent programs. In International Conference on Computer Aided Verification, pages 434–449, 2010.

Digital Library

[19]

S. Kundu, M. K. Ganai, and C. Wang. CONTESSA: Concurrency testing augmented with symbolic analysis. In International Conference on Computer Aided Verification, pages 127–131, 2010.

Digital Library

[20]

M. Kusano and C. Wang. Assertion guided abstraction: a cooperative optimization for dynamic partial order reduction. In IEEE/ACM International Conference On Automated Software Engineering, pages 175–186, 2014.

Digital Library

[21]

S. K. Lahiri, K. L. McMillan, R. Sharma, and C. Hawblitzel. Differential assertion checking. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 345–355, 2013.

Digital Library

[22]

M. S. Lam, J. Whaley, V. B. Livshits, M. C. Martin, D. Avots, M. Carbin, and C. Unkel. Context-sensitive program analysis as database queries. In ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, pages 1–12, 2005.

Digital Library

[23]

C. Lattner and V. Adve. The LLVM Compiler Framework and Infrastructure Tutorial. In LCPC’04 Mini Workshop on Compiler Research Infrastructures, West Lafayette, Indiana, Sep 2004.

Digital Library

[24]

S. Lehnert. A taxonomy for software change impact analysis. In International Workshop on Principles of Software Evolution, pages 41–50, 2011.

Digital Library

[25]

L. Li and C. Wang. Dynamic analysis and debugging of binary code for security applications. In International Conference on Runtime Verification, pages 403–423, 2013.

[26]

K. L. McMillan. Lazy annotation for program testing and verification. In International Conference on Computer Aided Verification, pages 104–118, 2010.

Digital Library

[27]

M. Naik and A. Aiken. Conditional must not aliasing for static race detection. SIGPLAN Not., 42(1):327–338, Jan. 2007.

Digital Library

[28]

M. Naik, A. Aiken, and J. Whaley. Effective static race detection for java. SIGPLAN Not., 41(6):308–319, June 2006.

Digital Library

[29]

Non-blocking data structures.

[30]

S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed incremental symbolic execution. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 504–515, 2011.

Digital Library

[31]

S. Raghavan, R. Rohana, D. Leon, A. Podgurski, and V. Augustine. Dex: A semantic-graph differencing tool for studying changes in large code bases. In IEEE International Conference on Software Maintenance, pages 188–197, 2004.

Digital Library

[32]

N. Rungta, S. Person, and J. Branchaud. A change impact analysis to characterize evolving program behaviors. In IEEE International Conference on Software Maintenance, pages 109–118, 2012.

Digital Library

[33]

K. Sen. Scalable Automated Methods for Dynamic Program Analysis. PhD thesis, UIUC, 2006.

Digital Library

[34]

N. Sinha and C. Wang. Staged concurrent program analysis. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 47–56, 2010.

Digital Library

[35]

N. Sinha and C. Wang. On interference abstractions. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 423–434, 2011.

Digital Library

[36]

W. N. Sumner, C. Hammer, and J. Dolby. Marathon: Detecting atomic-set serializability violations with conflict graphs. In International Conference on Runtime Verification, pages 161–176, 2012.

Digital Library

[37]

SV-COMP. 2015 software verification competition.

[38]

V. Terragni, S.-C. Cheung, and C. Zhang. RECONTEST: Effective regression testing of concurrent programs. In International Conference on Software Engineering, 2015.

Digital Library

[39]

M. Vaziri, F. Tip, and J. Dolby. Associating synchronization constraints with data in an object-oriented language. In J. G. Morrisett and S. L. P. Jones, editors, ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 334–345. ACM, 2006.

Digital Library

[40]

C. Wang, S. Chaudhuri, A. Gupta, and Y. Yang. Symbolic pruning of concurrent program executions. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 23–32, 2009.

Digital Library

[41]

C. Wang, S. Kundu, M. Ganai, and A. Gupta. Symbolic predictive analysis for concurrent programs. In International Symposium on Formal Methods, pages 256–272, 2009.

Digital Library

[42]

C. Wang, Z. Yang, V. Kahlon, and A. Gupta. Peephole partial order reduction. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 382–396, 2008.

Digital Library

[43]

M. Weiser. Program slicing. In International Conference on Software Engineering, pages 439–449, Piscataway, NJ, USA, 1981. IEEE Press.

Digital Library

[44]

J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 131–144, 2004.

Digital Library

[45]

J. W. Wilkerson. A software change impact analysis taxonomy. In IEEE International Conference on Software Maintenance, pages 625–628, 2012.

Digital Library

[46]

G. Yang, S. Khurshid, S. Person, and N. Rungta. Property differencing for incremental checking. In International Conference on Software Engineering, pages 1059–1070, 2014.

Digital Library

[47]

W. Yang. Identifying syntactic differences between two programs. Softw., Pract. Exper., 21(7):739–755, 1991.

Digital Library

[48]

Q. Yi, Z. Yang, S. Guo, C. Wang, J. Liu, and C. Zhao. Postconditioned symbolic execution. In IEEE International Conference on Software Testing, Verification and Validation, pages 1–10, 2015.

[49]

T. Yu, W. Srisa-an, and G. Rothermel. SimRT: an automated framework to support regression testing for data races. In International Conference on Software Engineering, pages 48–59, 2014.

Digital Library

Cited By

Ding ZLi SChen CHe C(2025)Program Dependence Net and on-demand slicing for property verification of concurrent system and softwareJournal of Systems and Software10.1016/j.jss.2024.112221219:COnline publication date: 1-Jan-2025
https://dl.acm.org/doi/10.1016/j.jss.2024.112221
Sun XGupta RBond MLee JPayer H(2024)SSRD: Shapes and Summaries for Race Detection in Concurrent Data StructuresProceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management10.1145/3652024.3665505(68-81)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652024.3665505
Shahbaz M(2023)An Approach for Test Impact Analysis on the Integration Level in Java ProgramsProceedings of Eighth International Congress on Information and Communication Technology10.1007/978-981-99-3091-3_14(171-188)Online publication date: 30-Jul-2023
https://doi.org/10.1007/978-981-99-3091-3_14
Show More Cited By

Index Terms

Conc-iSE: incremental symbolic execution of concurrent software
1. Software and its engineering
  1. Software creation and management
    1. Software post-development issues
      1. Software evolution
    2. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Enhancing symbolic execution with veritesting
ICSE 2014: Proceedings of the 36th International Conference on Software Engineering

We present MergePoint, a new binary-only symbolic execution system for large-scale and fully unassisted testing of commodity off-the-shelf (COTS) software. MergePoint introduces veritesting, a new technique that employs static symbolic execution to ...
Assertion guided symbolic execution of multithreaded programs
ESEC/FSE 2015: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering

Symbolic execution is a powerful technique for systematic testing of sequential and multithreaded programs. However, its application is limited by the high cost of covering all feasible intra-thread paths and inter-thread interleavings. We propose a ...
Runtime exception detection in Java programs using symbolic execution

Most of the runtime failures of a software system can be revealed during test execution only, which has a very high cost. In Java programs, runtime failures are manifested as unhandled runtime exceptions.

In this paper we present an approach and tool ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '16: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering

August 2016

899 pages

ISBN:9781450338455

DOI:10.1145/2970276

General Chair:
David Lo
Singapore Management University, Singapore
,
Program Chairs:
Sven Apel
University of Passau, Germany
,
Sarfraz Khurshid
University of Texas at Austin, USA

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

SIGAI: ACM Special Interest Group on Artificial Intelligence
SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 August 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ASE'16

Sponsor:

SIGAI
SIGSOFT
IEEE-CS

ASE'16: ACM/IEEE International Conference on Automated Software Engineering

September 3 - 7, 2016

Singapore, Singapore

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

34
Total Citations
View Citations
364
Total Downloads

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

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ding ZLi SChen CHe C(2025)Program Dependence Net and on-demand slicing for property verification of concurrent system and softwareJournal of Systems and Software10.1016/j.jss.2024.112221219:COnline publication date: 1-Jan-2025
https://dl.acm.org/doi/10.1016/j.jss.2024.112221
Sun XGupta RBond MLee JPayer H(2024)SSRD: Shapes and Summaries for Race Detection in Concurrent Data StructuresProceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management10.1145/3652024.3665505(68-81)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652024.3665505
Shahbaz M(2023)An Approach for Test Impact Analysis on the Integration Level in Java ProgramsProceedings of Eighth International Congress on Information and Communication Technology10.1007/978-981-99-3091-3_14(171-188)Online publication date: 30-Jul-2023
https://doi.org/10.1007/978-981-99-3091-3_14
Li SChen CHuang ZDing Z(2023)Change‐aware model checking for evolving concurrent programs based on Program Dependence NetJournal of Software: Evolution and Process10.1002/smr.2626Online publication date: 9-Nov-2023
https://doi.org/10.1002/smr.2626
He FYu QCai L(2022)Efficient Summary Reuse for Software Regression VerificationIEEE Transactions on Software Engineering10.1109/TSE.2020.302147748:4(1417-1431)Online publication date: 1-Apr-2022
https://doi.org/10.1109/TSE.2020.3021477
Liu YXu ZFan MHao YChen KChen HCai YYang ZLiu T(2022)ConcSpectre: Be Aware of Forthcoming Malware Hidden in Concurrent ProgramsIEEE Transactions on Reliability10.1109/TR.2022.316269471:2(1174-1188)Online publication date: Jun-2022
https://doi.org/10.1109/TR.2022.3162694
Bose PDas DChen YFeng YKruegel CVigna G(2022)SAILFISH: Vetting Smart Contract State-Inconsistency Bugs in Seconds2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833721(161-178)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833721
Duan ZLi YMa PGou XYang S(2022)A Multi-Layer Fault Triggering Framework based on Evolutionary Strategy Guided Symbolic Execution for Automated Test Case Generation2022 IEEE 22nd International Conference on Software Quality, Reliability, and Security Companion (QRS-C)10.1109/QRS-C57518.2022.00045(255-262)Online publication date: Dec-2022
https://doi.org/10.1109/QRS-C57518.2022.00045
Yi QYang G(2022)Feedback-Driven Incremental Symbolic Execution2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE55969.2022.00055(505-516)Online publication date: Oct-2022
https://doi.org/10.1109/ISSRE55969.2022.00055
Steinhöfel D(2022)Symbolic Execution: Foundations, Techniques, Applications, and Future PerspectivesThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_22(446-480)Online publication date: 4-Jul-2022
https://doi.org/10.1007/978-3-031-08166-8_22
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.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten