Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Journal articles
  4. Efficient State Merging in Symbolic Execution
 
research article

Efficient State Merging in Symbolic Execution

Kuznetsov, Volodymyr  
•
Kinder, Johannes  
•
Bucur, Stefan  
Show more
2012
Acm Sigplan Notices

Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. Nevertheless, due to state explosion, these tools still struggle to achieve scalability. Given a program, one way to reduce the number of states that the tools need to explore is to merge states obtained on different paths. Alas, doing so increases the size of symbolic path conditions (thereby stressing the underlying constraint solver) and interferes with optimizations of the exploration process (also referred to as search strategies). The net effect is that state merging may actually lower performance rather than increase it. We present a way to automatically choose when and how to merge states such that the performance of symbolic execution is significantly increased. First, we present query count estimation, a method for statically estimating the impact that each symbolic variable has on solver queries that follow a potential merge point; states are then merged only when doing so promises to be advantageous. Second, we present dynamic state merging, a technique for merging states that interacts favorably with search strategies in automated test case generation and bug finding tools. Experiments on the 96 GNU COREUTILS show that our approach consistently achieves several orders of magnitude speedup over previously published results. Our code and experimental data are publicly available at http://cloud9.epfl.ch.

  • Details
  • Metrics
Type
research article
DOI
10.1145/2345156.2254088
Web of Science ID

WOS:000307582100018

Author(s)
Kuznetsov, Volodymyr  
Kinder, Johannes  
Bucur, Stefan  
Candea, George  
Date Issued

2012

Publisher

Assoc Computing Machinery

Published in
Acm Sigplan Notices
Volume

47

Issue

6

Start page

193

End page

204

Subjects

Testing

•

Symbolic Execution

•

Verification

•

Bounded Software Model Checking

•

State Merging

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
IIF  
Available on Infoscience
February 27, 2013
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/89805
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés