Controlling factors in evaluating path-sensitive error detection techniques

ABSTRACT

Recent advances in static program analysis have made it possible to detect errors in applications that have been thoroughly tested and are in wide-spread use. The ability to find errors that have eluded traditional validation methods is due to the development and combination of sophisticated algorithmic techniques that are embedded in the implementations of analysis tools. Evaluating new analysis techniques is typically performed by running an analysis tool on a collection of subject programs, perhaps enabling and disabling a given technique in different runs. While seemingly sensible, this approach runs the risk of attributing improvements in the cost-effectiveness of the analysis to the technique under consideration, when those improvements may actually be due to details of analysis tool implementations that are uncontrolled during evaluation.In this paper, we focus on the specific class of path-sensitive error detection techniques and identify several factors that can significantly influence the cost of analysis. We show, through careful empirical studies, that the influence of these factors is sufficiently large that, if left uncontrolled, they may lead researchers to improperly attribute improvements in analysis cost and effectiveness. We make several recommendations as to how the influence of these factors can be mitigated when evaluating techniques.

REFERENCES

• 1: James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996 [doi>10.1109/32.489078]
• 2: J. C. Corbett, M. B. Dwyer, J. Hatcliff, and Robby. Expressing checkable properties of dynamic systems: The Bandera Specification Language. International Journal on Software Tools for Technology Transfer, 2002.
• 3: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 4: H. Do, S. G. Elbaum, and G. Rothermel. Subject infrastructure repository. http://esquared.unl.edu/sir.
• 5: Y. Dong, X. Du, G. J. Holzmenn, and S. A. Smolka. Fighting livelock in the gnu i-protocol: a case study in explicit-state model checking. Int'l. Journal on Software Tools for Tech. Transfer, 4(4):505--528, 2003.
• 6: M. B. Dwyer, J. Hatcliff, M. Hoosier, V. Ranganath, Robby, and T. Wallentine. Evaluating the effectiveness of program slicing for model reduction of concurrent object-oriented programs. In Proc. of the Twelfth Int'l. Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2006. LNCS 3920.
• 7: Matthew B. Dwyer , John Hatcliff , Robby , Venkatesh Prasad Ranganath, Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs, Formal Methods in System Design, v.25 n.2-3, p.199-240, September-November 2004 [doi>10.1023/B:FORM.0000040028.49845.67]
• 8: S. Edelkamp, S. Leue, and A. Lluch-Lafuente. Partial-order reduction and trail improvement in directed model checking. International Journal on Software Tools for Technology Transfer, 6(4), 2004.
• 9: http://home.att.net/~ddavies/NewSmulator.html.
• 10: Y. Eytani, K. Havelund, S. D. Stoller, and S. Ur. Toward a framework and benchmark for testing tools for multi-threaded programs. Concurrency and Computation: Practice and Experience, to appear.
• 11: Y. Eytani and S. Ur. Compiling a benchmark of documented multi-threaded bugs. In Proc. of the Workshop on Parallel and Distributed Systems: Testing and Debugging, 2004.
• 12: Eitan Farchi , Yarden Nir , Shmuel Ur, Concurrent Bug Patterns and How to Test Them, Proceedings of the 17th International Symposium on Parallel and Distributed Processing, p.286.2, April 22-26, 2003
• 13: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 14: A. Groce and W. Visser. Heuristics for model checking java programs. Int'l. Journal on Software Tools for Tech. Transfer, 6(4):260--276, 2004.
• 15: Dick Hamlet , Jeff Voas, Faults on its sleeve: amplifying software reliability testing, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.89-98, June 28-30, 1993, Cambridge, Massachusetts, United States
• 16: Klaus Havelund , Scott D. Stoller , Shmuel Ur, Benchmark and Framework for Encouraging Research on Multi-Threaded Testing Tools, Proceedings of the 17th International Symposium on Parallel and Distributed Processing, p.286.1, April 22-26, 2003
• 17: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 18: http://www.kclee.de/clemens/java/javancss.
• 19: M. Musuvathi and D. R. Engler. Model Checking Large Network Protocol Implementations. In Proc. of the First Symp. on Networked Systems Design and Implementation, Mar. 2004.
• 20: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

  Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

  , December 09-11, 2002, Boston, Massachusetts [doi>10.1145/1060289.1060297]
• 21: C. Păsăreanu, M. B. Dwyer, and W. Visser. Finding feasible abstract counter-examples. Int'l. Journal on Software Tools for Tech. Transfer, 5(1):34--48, 2003.
• 22: http://research.microsoft.com/qadeer/cav-issta.htm.
• 23: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 24: Robby, M. B. Dwyer, J. Hatcliff, and R. Iosif. Space-reduction strategies for model checking dynamic systems. In Proceedings of the 2003 Workshop on Software Model Checking, July 2003.
• 25: S. D. Stoller. Testing concurrent java programs using randomized scheduling. In Proc. Workshop on Runtime Verification, 2002.
• 26: Jianbin Tan , George S. Avrunin , Lori A. Clarke , Shlomo Zilberstein , Stefan Leue, Heuristic-guided counterexample search in FLAVERS, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 27: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 28: J. Yang, P. Twohey, D. R. Engler, and M. Musuvathi. Using Model Checking to Find Serious File System Errors. In Proc. of the Seventh Symp. on Operating Systems Design and Implementation, Dec. 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Experimentation, Verification

Keywords:
empirical study, model checking, path-sensitive analysis