More Web Proxy on the site http://driver.im/

research-article

Efficient modular glass box software model checking

Authors:

Michael Roberson,

Chandrasekhar BoyapatiAuthors Info & Claims

OOPSLA '10: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

Pages 4 - 21

https://doi.org/10.1145/1869459.1869461

Published: 17 October 2010 Publication History

Abstract

Glass box software model checking incorporates novel techniques to identify similarities in the state space of a model checker and safely prune large numbers of redundant states without explicitly checking them. It is significantly more efficient than other software model checking approaches for checking certain kinds of programs and program properties.

This paper presents Pipal, a system for modular glass box software model checking. Extending glass box software model checking to perform modular checking is important to further improve its scalability. It is nontrivial because unlike traditional software model checkers such as Java PathFinder (JPF) and CMC, a glass box software model checker does not check every state separately---instead, it checks a large set of states together in each step. We present a solution and demonstrate Pipal's effectiveness on a variety of programs.

References

[1]

}}T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In Programming Language Design and Implementation (PLDI), June 2001.

Digital Library

[2]

}}Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development. Springer Verlag, 2004.

Digital Library

[3]

}}C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates. In International Symposium on Software Testing and Analysis (ISSTA), July 2002.

Digital Library

[4]

}}S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In International Conference on Software Engineering (ICSE), June 2003.

Digital Library

[5]

}}E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.

Digital Library

[6]

}}E. M. Clarke, E. A. Emerson, and J. Sifakis. Model checking: Algorithmic verification and debugging. Communications of the ACM (CACM) 52(11), 2009.

Digital Library

[7]

}}J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In International Conference on Software Engineering (ICSE), June 2000.

Digital Library

[8]

}}P. Darga and C. Boyapati. Efficient software model checking of data structure properties. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2006.

Digital Library

[9]

}}C. DeMartini, R. Iosif, and R. Sisto. A deadlock detection tool for concurrent Java programs. Software-Practice and Experience (SPE) 29(7), June 1999.

Digital Library

[10]

}}X. Deng, J. Lee, and Robby. Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In Automated Software Engineering (ASE), September 2006.

Digital Library

[11]

}}G. Dennis, F. Chang, and D. Jackson. Modular verification of code with SAT. International Symposium on Software Testing and Analysis, 2006.

Digital Library

[12]

}}J. Dolby, M. Vaziri, and F. Tip. Finding bugs efficiently with a SAT solver. In European Software Engineering Conference and Foundations of Software Engineering (ESEC/FSE), September 2007.

Digital Library

[13]

}}M. Dwyer, J. Hatcliff, M. Hoosier, and Robby. Building your own software model checker using the Bogor extensible model checking framework. In Computer Aided Verification (CAV), January 2005.

Digital Library

[14]

}}N. Een and A. Biere. Effective preprocessing in SAT through variable and clause elimination. In Theory and Applications of Satisfiability Testing (SAT), June 2005.

Digital Library

[15]

}}C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In Principles of Programming Languages (POPL), January 2005.

Digital Library

[16]

}}P. Godefroid. Model checking for programming languages using VeriSoft. In Principles of Programming Languages (POPL), January 1997.

Digital Library

[17]

}}P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Programming Language Design and Implementation (PLDI), June 2005.

Digital Library

[18]

}}J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification, Third Edition. Addison-Wesley, 2005.

Digital Library

[19]

}}S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Computer Aided Verification (CAV), June 1997.

Digital Library

[20]

}}W. Grieskamp, N. Tillmann, and W. Shulte. XRT-Exploring runtime for .NET: Architecture and applications. In Workshop on Software Model Checking (SoftMC), July 2005.

[21]

}}T. A. Henzinger, R. Jhala, and R. Majumdar. Lazy abstraction. In Principles of Programming Languages (POPL), January 2002.

Digital Library

[22]

}}G. Holzmann. The model checker SPIN. Transactions on Software Engineering (TSE) 23(5), May 1997.

Digital Library

[23]

}}A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 1999.

Digital Library

[24]

}}R. Iosif. Symmetry reduction criteria for software model checking. In SPIN workshop on Model Checking of Software (SPIN), April 2002.

Digital Library

[25]

}}C. N. Ip and D. Dill. Better verification through symmetry. In Computer Hardware Description Languages, April 1993.

Digital Library

[26]

}}D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006.

Digital Library

[27]

}}D. Jackson and C. Damon. Elements of style: Analyzing a software design feature with a counterexample detector. IEEE Transactions on Software Engineering (TSE) 22(7), July 1996.

Digital Library

[28]

}}P. Joshi, M. Naik, C.-S. Park, and K. Sen. An extensible active testing framework for concurrent programs. Computer Aided Verification (CAV), 2009.

Digital Library

[29]

}}M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000.

Digital Library

[30]

}}S. Khurshid and D. Marinov. TestEra: Specification-based testing of Java programs using SAT. In Automated Software Engineering (ASE), November 2001.

Digital Library

[31]

}}S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2003.

Digital Library

[32]

}}S. Khurshid, D. Marinov, and D. Jackson. An analyzable annotation language. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), November 2002.

Digital Library

[33]

}}J. C. King. Symbolic execution and program testing. In Communications of the ACM (CACM) 19(7), August 1976.

Digital Library

[34]

}}B. Liskov and J. Guttag. Abstraction and Specification in Program Development. MIT Press, 1986.

Digital Library

[35]

}}D. Marinov, A. Andoni, D. Daniliuc, S. Khurshid, and M. Rinard. An evaluation of exhaustive testing for data structures. Technical Report TR-921, MIT Laboratory for Computer Science, September 2003.

[36]

}}K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

[37]

}}M. Musuvathi and D. Dill. An incremental heap canonicalization algorithm. In SPIN workshop on Model Checking of Software (SPIN), August 2005.

Digital Library

[38]

}}M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing heisenbugs in concurrent programs. Operating System Design and Implementation (OSDI), 2008.

Digital Library

[39]

}}M. Musuvathi, D. Y. W. Park, A. Chou, D. R. Engler, and D. Dill. CMC: A pragmatic approach to model checking real code. In Operating System Design and Implementation (OSDI), December 2002.

Digital Library

[40]

}}T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer Verlag, 2002.

Digital Library

[41]

}}N. Nystrom, M. R. Clarkson, and A. C. Myers. Polyglot: An extensible compiler framework for Java. In Compiler Construction (CC), April 2003.

Digital Library

[42]

}}J. Offutt and R. Untch. Mutation 2000: Uniting the orthogonal. In Mutation 2000: Mutation Testing in the Twentieth and the Twenty First Centuries, October 2000.

[43]

}}M. Roberson, M. Harries, P. T. Darga, and C. Boyapati. Efficient software model checking of soundness of type systems. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2008.

Digital Library

[44]

}}K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In European Software Engineering Conference and Foundations of Software Engineering (ESEC/FSE), September 2005.

Digital Library

[45]

}}D. Shao, S. Khurshid, and D. Perry. Whispec: White-box testing of libraries using declarative specifications. Library-Centric Software Design (LCSD), 2007.

Digital Library

[46]

}}M. Vaziri and D. Jackson. Checking properties of heap-manipulating procedures using a constraint solver. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2003.

Digital Library

[47]

}}W. Visser, C. S. Pasareanu, and S. Khurshid. Test input generation with Java PathFinder. In International Symposium on Software Testing and Analysis (ISSTA), July 2004.

Digital Library

[48]

}}W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In Automated Software Engineering (ASE), September 2000.

Digital Library

Cited By

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Chandra KBodik R(2017)Bonsai: synthesis-based reasoning for type systemsProceedings of the ACM on Programming Languages10.1145/31581502:POPL(1-34)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158150
Nokhbeh Zaeem RKhurshid STracz WRobillard MBultan T(2012)Test input generation using dynamic programmingProceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering10.1145/2393596.2393635(1-11)Online publication date: 11-Nov-2012
https://dl.acm.org/doi/10.1145/2393596.2393635
Show More Cited By

Recommendations

Efficient modular glass box software model checking
OOPSLA '10

Glass box software model checking incorporates novel techniques to identify similarities in the state space of a model checker and safely prune large numbers of redundant states without explicitly checking them. It is significantly more efficient than ...
Glass box software model checking
Efficient software model checking of data structure properties
Proceedings of the 2006 OOPSLA Conference

This paper presents novel language and analysis techniques that significantly speed up software model checking of data structure properties. Consider checking a red-black tree implementation. Traditional software model checkers systematically generate ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA '10: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

October 2010

984 pages

ISBN:9781450302036

DOI:10.1145/1869459

General Chairs:
William R. Cook
University of Texas at Austin
,
Siobhán Clarke
Trinity College Dublin
,
Program Chairs:
Martin Rinard
MIT
,
Kevin J. Sullivan
University of Virginia
,
Daniel H. Steinberg
Dim Sum Thinking Inc.

ACM SIGPLAN Notices Volume 45, Issue 10
OOPSLA '10
October 2010
957 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1932682
Issue’s Table of Contents

Copyright © 2010 ACM.

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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 October 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '10

Sponsor:

SIGPLAN

SPLASH '10: Systems Programming Languages and Applications: Software for Humanity

October 17 - 21, 2010

Nevada, Reno/Tahoe, USA

Acceptance Rates

Overall Acceptance Rate 268 of 1,244 submissions, 22%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
338
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Chandra KBodik R(2017)Bonsai: synthesis-based reasoning for type systemsProceedings of the ACM on Programming Languages10.1145/31581502:POPL(1-34)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158150
Nokhbeh Zaeem RKhurshid STracz WRobillard MBultan T(2012)Test input generation using dynamic programmingProceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering10.1145/2393596.2393635(1-11)Online publication date: 11-Nov-2012
https://dl.acm.org/doi/10.1145/2393596.2393635
Malik MKhurshid S(2012)Dynamic Shape Analysis Using Spectral Graph PropertiesProceedings of the 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation10.1109/ICST.2012.101(211-220)Online publication date: 17-Apr-2012
https://dl.acm.org/doi/10.1109/ICST.2012.101
Deng XLee JRobby (2012)Efficient and formal generalized symbolic executionAutomated Software Engineering10.1007/s10515-011-0089-919:3(233-301)Online publication date: 1-Sep-2012
https://dl.acm.org/doi/10.1007/s10515-011-0089-9
Yi QLiu JShen W(2011)Efficient Loop-Extended Model Checking of Data Structure MethodsSoftware Engineering, Business Continuity, and Education10.1007/978-3-642-27207-3_24(237-249)Online publication date: 2011
https://doi.org/10.1007/978-3-642-27207-3_24

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents