Guided model checking for programs with polymorphism

ABSTRACT

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.

REFERENCES

• 1: Cyrille Artho , Armin Biere, Applying Static Analysis to Large-Scale, Multi-Threaded Java Programs, Proceedings of the 13th Australian Conference on Software Engineering, p.68, August 27-28, 2001
• 2: David F. Bacon , Peter F. Sweeney, Fast static analysis of C++ virtual function calls, Proceedings of the 11th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.324-341, October 06-10, 1996, San Jose, California, United States
• 3: Thomas Ball , Sriram K. Rajamani, The SLAM Toolkit, Proceedings of the 13th International Conference on Computer Aided Verification, p.260-264, July 18-22, 2001
• 4: J. Burnim and K. Sen. Heuristics for scalable dynamic test generation. In 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), pages 443--446. IEEE, 2008.
• 5: Jamieson M. Cobleigh , Lori A. Clarke , Leon J. Osterweil, The right algorithm at the right time: comparing data flow analysis algorithms for finite state verification, Proceedings of the 23rd International Conference on Software Engineering, p.37-46, May 12-19, 2001, Toronto, Ontario, Canada
• 6: Matthew B. Dwyer , Suzette Person , Sebastian Elbaum, Controlling factors in evaluating path-sensitive error detection techniques, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181787]
• 7: S. Edelkamp and T. Mehler. Byte code distance heuristics and trail direction for model checking Java programs. In Workshop on Model Checking and Artificial Intelligence (MoChArt), pages 69--76, 2003.
• 8: S. Edelkamp, A. L. Lafuente, and S. Leue. Trail-directed model checking. In S. D. Stoller and W. Visser, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier Science Publishers, 2001a.
• 9: Stefan Edelkamp , Alberto Lluch Lafuente , Stefan Leue, Directed explicit model checking with HSF-SPIN, Proceedings of the 8th international SPIN workshop on Model checking of software, p.57-79, May 2001, Toronto, Ontario, Canada
• 10: 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
• 11: Alex Groce , Willem Visser, Model checking Java programs using structural heuristics, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 12: Craig Harvey , Paul Strooper, Testing Java Monitors through Deterministic Execution, Proceedings of the 13th Australian Conference on Software Engineering, p.61, August 27-28, 2001
• 13: Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.245-264, August 30-September 01, 2000
• 14: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In T. Ball and S.K.Rajamani, editors, Proceedings of the 10th International Workshop on Model Checking of Software (SPIN), volume 2648 of Lecture Notes in Computer Science, pages 235--239, Portland, OR, May 2003.
• 15: Gerard Holzmann, Spin model checker, the: primer and reference manual, Addison-Wesley Professional, 2003
• 16: David Hovemeyer , William Pugh, Finding bugs is easy, ACM SIGPLAN Notices, v.39 n.12, December 2004 [doi>10.1145/1052883.1052895]
• 17: Kuntal Nanshi , Fabio Somenzi, Guiding simulation with increasingly refined abstract traces, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1147097]
• 18: Flavio M. De Paula , Alan J. Hu, An effective guidance strategy for abstraction-guided simulation, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California [doi>10.1145/1278480.1278498]
• 19: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
• 20: Neha Rungta , Eric G. Mercer, A context-sensitive structural heuristic for guided search model checking, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101982]
• 21: Neha Rungta , Eric G. Mercer, An Improved Distance Heuristic Function for Directed Software Model Checking, Proceedings of the Formal Methods in Computer Aided Design, p.60-67, November 12-16, 2006 [doi>10.1109/FMCAD.2006.5]
• 22: N. Rungta and E. G. Mercer. A meta heuristic for effectively detecting concurrency errors. In Haifa Verification Conference, To Appear., Haifa, Israel, 2008.
• 23: Hardness for Explicit State Software Model Checking Benchmarks, Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods, p.247-256, September 10-14, 2007 [doi>10.1109/SEFM.2007.23]
• 24: N. Rungta and E. G. Mercer. Generating counter-examples through randomized guided search. In Proceedings of the 14th International SPIN Workshop on Model Checking of Software, pages 39--57, Berlin, Germany, July 2007b. Springer-Verlag.
• 25: Stuart J. Russell , Peter Norvig, Artificial intelligence: a modern approach, Prentice-Hall, Inc., Upper Saddle River, NJ, 1995
• 26: K. Sen and G. Agha. A race-detection and flipping algorithm for automated testing of multi-threaded programs. In Haifa Verification Conference, volume 4383 of Lecture Notes in Computer Science, pages 166--182. Springer, 2007. ISBN 978-3-540-70888-9.
• 27: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 28: Kevin Seppi , Michael Jones , Peter Lamborn, Guided model checking with a Bayesian meta-heuristic, Fundamenta Informaticae, v.70 n.1, p.111-126, October 2005
• 29: 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
• 30: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 31: C. Han Yang , David L. Dill, Validation with guided search of the state space, Proceedings of the 35th annual conference on Design automation, p.599-604, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277201]

INDEX TERMS

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

General Terms:
Reliability, Verification

Keywords:
error discovery, guided search, heuristics, software model checking