Exhaustive model checking search techniques are ineffective for error discovery in large and complex multi-threaded software systems. Distance estimate heuristics guide the concrete execution of the program toward a possible error location. The estimate is a lower-bound computed on a statically generated abstract model of the program that ignores all data values and only considers control flow. In this paper we describe a new distance estimate heuristic that efficiently computes a tighter lower-bound in programs with polymorphism when compared to the state of the art distance heuristic. We statically generate conservative distance estimates and refine the estimates when the targets of dynamic method invocations are resolved. In our empirical analysis the state of the art approach is computationally infeasible for large programs with polymorphism while our new distance heuristic can quickly detect the errors.

Pdf version or access through the ACM Portal

Conference Slides

N. Rungta and E. G. Mercer. Guided model checking for programs with polymorphism, ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), Savannah, January 2009.

@inproceedings{1480950,
  author = {Neha Rungta and Eric G Mercer},
  title = {Guided model checking for programs with polymorphism},
  booktitle = {PEPM '09: Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation},
  year = {2008},
  isbn = {978-1-60558-327-3},
  pages = {21--30},
  location = {Savannah, GA, USA},
  doi = {http://doi.acm.org/10.1145/1480945.1480950},
  publisher = {ACM},
  address = {New York, NY, USA},
 }