Concolic fault localization

Chanseok Oh, Martin Schaf, Daniel Schwartz-Narbonne, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

An integral part of all debugging activities is the task of diagnosing the cause of an error. Most existing fault diagnosis techniques rely on the availability of high quality test suites because they work by comparing failing and passing runs to identify the error cause. This limits their applicability. One alternative are techniques that statically analyze an error trace of the program without relying on additional passing runs to compare against. Particularly promising are novel proof-based approaches that leverage the advances in automated theorem proving to obtain an abstraction of the program that aids fault diagnostics. However, existing proof-based approaches still have practical limitations such as reduced scalability and dependence on complex mathematical models of programs. Such models are notoriously difficult to develop for real-world programs. Inspired by concolic testing, we propose a novel algorithm that integrates concrete execution and symbolic reasoning about the error trace to address these challenges. Specifically, we execute the error trace to obtain intermediate program states that allow us to split the trace into smaller fragments, each of which can be analyzed in isolation using an automated theorem prover. Moreover, we show how this approach can avoid complex logical encodings when reasoning about traces in low-level C programs. We have conducted an experiment where we applied our new algorithm to error traces generated from faulty versions of UNIX utils such as gzip and sed. Our experiment indicates that our concolic fault abstraction scales to real-world error traces and generates useful error diagnoses.

Original languageEnglish (US)
Title of host publicationProceedings - 2014 14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages135-144
Number of pages10
ISBN (Print)9780769553047
DOIs
StatePublished - Dec 4 2014
Event14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014 - Victoria, Canada
Duration: Sep 28 2014Sep 29 2014

Other

Other14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014
CountryCanada
CityVictoria
Period9/28/149/29/14

Fingerprint

Theorem proving
UNIX
Failure analysis
Scalability
Experiments
Availability
Concretes
Mathematical models
Testing

Keywords

  • concolic execution
  • debugging
  • fault localization
  • interpolation

ASJC Scopus subject areas

  • Software
  • Computer Science Applications

Cite this

Oh, C., Schaf, M., Schwartz-Narbonne, D., & Wies, T. (2014). Concolic fault localization. In Proceedings - 2014 14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014 (pp. 135-144). [6975647] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/SCAM.2014.22

Concolic fault localization. / Oh, Chanseok; Schaf, Martin; Schwartz-Narbonne, Daniel; Wies, Thomas.

Proceedings - 2014 14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014. Institute of Electrical and Electronics Engineers Inc., 2014. p. 135-144 6975647.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Oh, C, Schaf, M, Schwartz-Narbonne, D & Wies, T 2014, Concolic fault localization. in Proceedings - 2014 14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014., 6975647, Institute of Electrical and Electronics Engineers Inc., pp. 135-144, 14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014, Victoria, Canada, 9/28/14. https://doi.org/10.1109/SCAM.2014.22
Oh C, Schaf M, Schwartz-Narbonne D, Wies T. Concolic fault localization. In Proceedings - 2014 14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014. Institute of Electrical and Electronics Engineers Inc. 2014. p. 135-144. 6975647 https://doi.org/10.1109/SCAM.2014.22
Oh, Chanseok ; Schaf, Martin ; Schwartz-Narbonne, Daniel ; Wies, Thomas. / Concolic fault localization. Proceedings - 2014 14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014. Institute of Electrical and Electronics Engineers Inc., 2014. pp. 135-144
@inproceedings{c7ae05abaa0d471690ae74e9534de9e3,
title = "Concolic fault localization",
abstract = "An integral part of all debugging activities is the task of diagnosing the cause of an error. Most existing fault diagnosis techniques rely on the availability of high quality test suites because they work by comparing failing and passing runs to identify the error cause. This limits their applicability. One alternative are techniques that statically analyze an error trace of the program without relying on additional passing runs to compare against. Particularly promising are novel proof-based approaches that leverage the advances in automated theorem proving to obtain an abstraction of the program that aids fault diagnostics. However, existing proof-based approaches still have practical limitations such as reduced scalability and dependence on complex mathematical models of programs. Such models are notoriously difficult to develop for real-world programs. Inspired by concolic testing, we propose a novel algorithm that integrates concrete execution and symbolic reasoning about the error trace to address these challenges. Specifically, we execute the error trace to obtain intermediate program states that allow us to split the trace into smaller fragments, each of which can be analyzed in isolation using an automated theorem prover. Moreover, we show how this approach can avoid complex logical encodings when reasoning about traces in low-level C programs. We have conducted an experiment where we applied our new algorithm to error traces generated from faulty versions of UNIX utils such as gzip and sed. Our experiment indicates that our concolic fault abstraction scales to real-world error traces and generates useful error diagnoses.",
keywords = "concolic execution, debugging, fault localization, interpolation",
author = "Chanseok Oh and Martin Schaf and Daniel Schwartz-Narbonne and Thomas Wies",
year = "2014",
month = "12",
day = "4",
doi = "10.1109/SCAM.2014.22",
language = "English (US)",
isbn = "9780769553047",
pages = "135--144",
booktitle = "Proceedings - 2014 14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - GEN

T1 - Concolic fault localization

AU - Oh, Chanseok

AU - Schaf, Martin

AU - Schwartz-Narbonne, Daniel

AU - Wies, Thomas

PY - 2014/12/4

Y1 - 2014/12/4

N2 - An integral part of all debugging activities is the task of diagnosing the cause of an error. Most existing fault diagnosis techniques rely on the availability of high quality test suites because they work by comparing failing and passing runs to identify the error cause. This limits their applicability. One alternative are techniques that statically analyze an error trace of the program without relying on additional passing runs to compare against. Particularly promising are novel proof-based approaches that leverage the advances in automated theorem proving to obtain an abstraction of the program that aids fault diagnostics. However, existing proof-based approaches still have practical limitations such as reduced scalability and dependence on complex mathematical models of programs. Such models are notoriously difficult to develop for real-world programs. Inspired by concolic testing, we propose a novel algorithm that integrates concrete execution and symbolic reasoning about the error trace to address these challenges. Specifically, we execute the error trace to obtain intermediate program states that allow us to split the trace into smaller fragments, each of which can be analyzed in isolation using an automated theorem prover. Moreover, we show how this approach can avoid complex logical encodings when reasoning about traces in low-level C programs. We have conducted an experiment where we applied our new algorithm to error traces generated from faulty versions of UNIX utils such as gzip and sed. Our experiment indicates that our concolic fault abstraction scales to real-world error traces and generates useful error diagnoses.

AB - An integral part of all debugging activities is the task of diagnosing the cause of an error. Most existing fault diagnosis techniques rely on the availability of high quality test suites because they work by comparing failing and passing runs to identify the error cause. This limits their applicability. One alternative are techniques that statically analyze an error trace of the program without relying on additional passing runs to compare against. Particularly promising are novel proof-based approaches that leverage the advances in automated theorem proving to obtain an abstraction of the program that aids fault diagnostics. However, existing proof-based approaches still have practical limitations such as reduced scalability and dependence on complex mathematical models of programs. Such models are notoriously difficult to develop for real-world programs. Inspired by concolic testing, we propose a novel algorithm that integrates concrete execution and symbolic reasoning about the error trace to address these challenges. Specifically, we execute the error trace to obtain intermediate program states that allow us to split the trace into smaller fragments, each of which can be analyzed in isolation using an automated theorem prover. Moreover, we show how this approach can avoid complex logical encodings when reasoning about traces in low-level C programs. We have conducted an experiment where we applied our new algorithm to error traces generated from faulty versions of UNIX utils such as gzip and sed. Our experiment indicates that our concolic fault abstraction scales to real-world error traces and generates useful error diagnoses.

KW - concolic execution

KW - debugging

KW - fault localization

KW - interpolation

UR - http://www.scopus.com/inward/record.url?scp=84924866854&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84924866854&partnerID=8YFLogxK

U2 - 10.1109/SCAM.2014.22

DO - 10.1109/SCAM.2014.22

M3 - Conference contribution

SN - 9780769553047

SP - 135

EP - 144

BT - Proceedings - 2014 14th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2014

PB - Institute of Electrical and Electronics Engineers Inc.

ER -