skip to main content
10.1145/1480945.1480950acmconferencesArticle/Chapter ViewAbstractPublication PagespepmConference Proceedingsconference-collections
research-article

Guided model checking for programs with polymorphism

Published: 19 January 2009 Publication History

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]
C. Artho and A. Biere. Applying static analysis to large-scale, multi-threaded java programs. In ASWEC '01: Proceedings of the 13th Australian Conference on Software Engineering, page 68, Washington, DC, USA, 2001. IEEE Computer Society.
[2]
D. F. Bacon and P. F. Sweeney. Fast static analysis of c++ virtual function calls. In OOPSLA '96: Proceedings of the 11th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pages 324--341, New York, NY, USA, 1996. ACM. ISBN 0-89791-788-X.
[3]
T. Ball and S. Rajamani. The SLAM toolkit. In G. Berry, H. Comon, and A. Finkel, editors, 13th Annual Conference on Computer Aided Verification (CAV 2001), volume 2102 of Lecture Notes in Computer Science, pages 260--264, Paris, France, July 2001. Springer-Verlag.
[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]
J. M. Cobleigh, L. A. Clarke, and L. J. Osterweil. The right algorithm at the right time: Comparing data flow analysis algorithms for finite state verification. In International Conference on Software Engineering, pages 37--46, 2001. URL citeseer.ist.psu.edu/cobleigh01right.html.
[6]
M. B. Dwyer, S. Person, and S. Elbaum. Controlling factors in evaluating path-sensitive error detection techniques. In SIGSOFT '06/FSE-14: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 92--104, New York, NY, USA, 2006. ACM Press. ISBN 1-59593-468-5.
[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]
S. Edelkamp, A. L. Lafuente, and S. Leue. Directed explicit model checking with HSF-SPIN. In Proceedings of the 7th International SPIN Workshop, number 2057 in Lecture Notes in Computer Science. Springer-Verlag, 2001b.
[10]
E. Farchi, Y. Nir, and S. Ur. Concurrent bug patterns and how to test them. In IPDPS '03: Proceedings of the 17th International Symposium on Parallel and Distributed Processing, page 286.2, Washington, DC, USA, 2003. IEEE Computer Society. ISBN 0-7695-1926-1.
[11]
A. Groce and W. Visser. Model checking Java programs using structural heuristics. In 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 12--21, 2002.
[12]
C. Harvey and P. Strooper. Testing Java monitors through deterministic execution. In ASWEC '01: Proceedings of the 13th Australian Conference on Software Engineering, page 61, Washington, DC, USA, 2001. IEEE Computer Society.
[13]
K. Havelund. Using runtime analysis to guide model checking of java programs. In Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, pages 245--264, London, UK, 2000. Springer-Verlag. ISBN 3-540-41030-9.
[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]
G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.
[16]
D. Hovemeyer and W. Pugh. Finding bugs is easy. SIGPLAN Not., 39(12): 92--106, 2004. ISSN 0362-1340.
[17]
K. Nanshi and F. Somenzi. Guiding simulation with increasingly refined abstract traces. In DAC '06: Proceedings of the 43rd annual conference on Design automation, pages 737--742, New York, NY, USA, 2006. ACM. ISBN 1-59593-381-6.
[18]
F. M. De Paula and A. J. Hu. An effective guidance strategy for abstraction-guided simulation. In Design Automation Conference (DAC), pages 63--68, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-627-1.
[19]
Robby, M. B. Dwyer, and J. Hatcliff. Bogor: An extensible and highly-modular model checking framework. ACM SIGSOFT Software Engineering Notes, 28(5): 267--276, September 2003.
[20]
N. Rungta and E. G. Mercer. A context-sensitive structural heuristic for guided search model checking. In 20th IEEE/ACM International Conference on Automated Software Engineering, pages 410--413, Long Beach, California, USA, November 2005.
[21]
N. Rungta and E. G. Mercer. An improved distance heuristic function for directed software model checking. In FMCAD '06: Proceedings of the Formal Methods in Computer Aided Design, pages 60--67, Washington, DC, USA, 2006. IEEE Computer Society. ISBN 0-7695-2707-8.
[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]
N. Rungta and E. G. Mercer. Hardness for explicit state software model checking benchmarks. In 5th IEEE International Conference on Software Engineering and Formal Methods, pages 247--256, London, U.K, September 2007a.
[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]
S.J. Russell, P. Norvig, J.F. Canny, J. Malik, and D.D. Edwards. Artificial intelligence: a modern approach. Prentice Hall Englewood Cliffs, 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]
K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for C. In ESEC/FSE-13: Proceedings of the 10th European software engineering conference, pages 263--272, New York, NY, USA, 2005. ACM. ISBN 1-59593-014-0.
[28]
K. Seppi, M. Jones, and P. Lamborn. Guided model checking with a bayesian meta-heuristic. Fundamenta Informaticae, 70(1-2): 111--126, 2006.
[29]
J. Tan, G. S. Avrunin, L. A. Clarke, S. Zilberstein, and S. Leue. Heuristic-guided counterexample search in flavers. In SIGSOFT '04/FSE-12: Proceedings of the 12th ACM SIGSOFT Twelfth International Symposium on Foundations of Software Engineering, pages 201--210, New York, NY, USA, 2004. ACM Press. ISBN 1-58113-855-5.
[30]
W. Visser, K. Havelund, G. P. Brat, S. Park, and F. Lerda. Model checking programs. Automated Software Engineering, 10(2): 203--232, 2003.
[31]
C. H. Yang and D. L. Dill. Validation with guided search of the state space. In 35th Design Automation Conference (DAC98), pages 599--604, 1998.

Cited By

View all
  • (2015)JCHARMING: A bug reproduction approach using crash traces and directed model checking2015 IEEE 22nd International Conference on Software Analysis, Evolution, and Reengineering (SANER)10.1109/SANER.2015.7081820(101-110)Online publication date: Mar-2015
  • (2010)GAMBITACM SIGPLAN Notices10.1145/1837853.169345845:5(15-24)Online publication date: 9-Jan-2010
  • (2010)GAMBITProceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/1693453.1693458(15-24)Online publication date: 9-Jan-2010
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PEPM '09: Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation
January 2009
208 pages
ISBN:9781605583273
DOI:10.1145/1480945
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 January 2009

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. error discovery
  2. guided search
  3. heuristics
  4. software model checking

Qualifiers

  • Research-article

Conference

PEPM '09
Sponsor:
PEPM '09: Partial Evaluation and Program Manipulation
January 19 - 20, 2009
GA, Savannah, USA

Acceptance Rates

Overall Acceptance Rate 66 of 120 submissions, 55%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)0
Reflects downloads up to 13 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2015)JCHARMING: A bug reproduction approach using crash traces and directed model checking2015 IEEE 22nd International Conference on Software Analysis, Evolution, and Reengineering (SANER)10.1109/SANER.2015.7081820(101-110)Online publication date: Mar-2015
  • (2010)GAMBITACM SIGPLAN Notices10.1145/1837853.169345845:5(15-24)Online publication date: 9-Jan-2010
  • (2010)GAMBITProceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/1693453.1693458(15-24)Online publication date: 9-Jan-2010
  • (2009)Clash of the TitansProceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging10.1145/1639622.1639631(1-10)Online publication date: 19-Jul-2009
  • (2009)Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic ExecutionProceedings of the 16th International SPIN Workshop on Model Checking Software10.1007/978-3-642-02652-2_16(174-191)Online publication date: 26-Jun-2009
  • (2009)A Meta Heuristic for Effectively Detecting Concurrency ErrorsProceedings of the 4th International Haifa Verification Conference on Hardware and Software: Verification and Testing10.1007/978-3-642-01702-5_8(23-37)Online publication date: 19-Apr-2009

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media