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. Conferences, Workshops, Symposiums, and Seminars
  4. Selective Symbolic Execution
 
conference paper

Selective Symbolic Execution

Chipounov, Vitaly  
•
Georgescu, Vlad
•
Zamfir, Cristian  
Show more
2009
Proceedings of the 5th Workshop on Hot Topics in System Dependability (HotDep)
5th Workshop on Hot Topics in System Dependability (HotDep)

Symbolic execution is a powerful technique for analyzing program behavior, finding bugs, and generating tests, but suffers from severely limited scalability: the largest programs that can be symbolically executed today are on the order of thousands of lines of code. To ensure feasibility of symbolic execution, even small programs must curtail their interactions with libraries, the operating system, and hardware devices. This paper introduces selective symbolic execution, a technique for creating the illusion of full-system symbolic execution, while symbolically running only the code that is of interest to the developer. We describe a prototype that can symbolically execute arbitrary portions of a full system, including applications, libraries, operating system, and device drivers. It seamlessly transitions back and forth between symbolic and concrete execution, while transparently converting system state from symbolic to concrete and back. Our technique makes symbolic execution practical for large software that runs in real environments, without requiring explicit modeling of these environments.

  • Files
  • Details
  • Metrics
Type
conference paper
Author(s)
Chipounov, Vitaly  
Georgescu, Vlad
Zamfir, Cristian  
Candea, George  
Date Issued

2009

Published in
Proceedings of the 5th Workshop on Hot Topics in System Dependability (HotDep)
Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
DSLAB  
Event nameEvent placeEvent date
5th Workshop on Hot Topics in System Dependability (HotDep)

Estoril, Portugal

2009-06-30

Available on Infoscience
July 9, 2009
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/41254
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