kirancodes.me
To Proof Maintenance & Beyond!
ASE 2011

BEST: A symbolic testing tool for predicting multi-threaded program failures

Malay K. Ganai, Nipun Arora, Chao Wang, Aarti Gupta, Gogul Balakrishnan

DOI 10.1109/ase.2011.6100134dblp

Abstract

We present a tool BEST (Binary instrumentation-based Error-directed Symbolic Testing) for predicting concurrency violations.1We automatically infer potential concurrency violations such as atomicity violations from an observed run of a multi-threaded program, and use precise modeling and constraint-based symbolic (non-enumerative) search to find feasible violating schedules in a generalization of the observed run. We specifically focus on tool scalability by devising POR-based simplification steps to reduce the formula and the search space by several orders-of-magnitude. We have successfully applied the tool to several publicly available C/C++/Java programs and found several previously known/unknown concurrency related bugs. The tool also has extensive visual support for debugging.

BibTeX
@inproceedings{Ganai-al:ASE11,
  author    = {Malay K. Ganai and
               Nipun Arora and
               Chao Wang and
               Aarti Gupta and
               Gogul Balakrishnan},
  title     = {{BEST:} A symbolic testing tool for predicting multi-threaded program failures},
  booktitle = {ASE},
  pages     = {596--599},
  publisher = {{IEEE} Computer Society},
  year      = {2011},
}

Related papers