Model checking sequential software programs via mixed symbolic analysis

ABSTRACT

We present an efficient symbolic search algorithm for software model checking. Our algorithms perform word-level reasoning by using a combination of decision procedures in Boolean and integer and real domains, and use novel symbolic search strategies optimized specifically for sequential programs to improve scalability. Experiments on real-world C programs show that the new symbolic search algorithms can achieve several orders-of-magnitude improvements over existing methods based on bit-level (Boolean) reasoning.

REFERENCES

• 1: Alfred V. Aho , Monica S. Lam , Ravi Sethi , Jeffrey D. Ullman, Compilers: Principles, Techniques, and Tools (2nd Edition), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2006
• 2: Paul Anderson , Thomas Reps , Tim Teitelbaum , Mark Zarins, Tool Support for Fine-Grained Software Inspection, IEEE Software, v.20 n.4, p.42-50, July 2003 [doi>10.1109/MS.2003.1207453]
• 3: Armando, A., Benerecetti, M., and Mantovani, J. 2006a. Model checking linear programs with arrays. Electr. Notes Theor. Comput. Sci. 144, 3, 79--94.
• 4: Armando, A., Mantovani, J., and Platania, L. 2006b. Bounded model checking of software using smt solvers instead of sat solvers. In Proceedings of SPIN. 146--162.
• 5: Eugene Asarin , Thao Dang , Oded Maler , Olivier Bournez, Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems, Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control, p.20-31, March 23-25, 2000
• 6: Roberto Bagnara , Elisa Ricci , Enea Zaffanella , Patricia M. Hill, Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library, Proceedings of the 9th International Symposium on Static Analysis, p.213-229, September 17-20, 2002
• 7: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 8: Bensalem, S., Ganesh, V., Lakhnech, Y., Munoz, C., Owre, S., Rueb, H., Rushby, J., Rusu, V., Saidi, H., Shankar, N., Singerman, E., and Tiwari, A. 2000. An overview of SAL. In Proceedings of the 5^th Langley Formal Methods Workshop.
• 9: Dirk Beyer , Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, The software model checker Blast: Applications to software engineering, International Journal on Software Tools for Technology Transfer (STTT), v.9 n.5, p.505-525, October 2007 [doi>10.1007/s10009-007-0044-z]
• 10: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 11: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 12: Tevfik Bultan , Richard Gerber , Christopher League, Composite model-checking: verification with type-specific symbolic representations, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.3-50, Jan. 2000 [doi>10.1145/332740.332746]
• 13: Tevfik Bultan , Richard Gerber , William Pugh, Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic, Proceedings of the 9th International Conference on Computer Aided Verification, p.400-411, June 22-25, 1997
• 14: J. R. Burch , E. M. Clarke , D. E. Long, Representing circuits more efficiently in symbolic model checking, Proceedings of the 28th conference on ACM/IEEE design automation, p.403-407, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127702]
• 15: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 16: Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Stefano Quer, Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits, Proceedings of the 34th annual conference on Design automation, p.728-733, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266355]
• 17: Cardelli, L. 1997. Type systems. In Handbook of Computer Science and Engineering.
• 18: Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 19: Clarke, E., Grumberg, O., and Peled, D. 2000. Model Checking. MIT Press.
• 20: Clarke, E., Kroening, D., and Lerda, F. 2004a. A tool for checking ANSI-C programs. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2988, Springer, 168--176.
• 21: Clarke, E., Kroening, D., and Lerda, F. 2004b. A tool for checking ANSI-C programs. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. K. Jensen and A. Podelski, Eds. Lecture Notes in Computer Science, vol. 2988. Springer, 168--176.
• 22: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 23: Cousot, P. and Cousot, R. 1976. Static determination of dynamic properties of programs. In Proceedings of the the 2^nd International Symposium on Programming.
• 24: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 25: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 26: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 27: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 28: Nicolas Halbwachs , Yann-Erick Proy , Patrick Roumanoff, Verification of Real-Time Systems using Linear Relation Analysis, Formal Methods in System Design, v.11 n.2, p.157-185, Aug. 1997 [doi>10.1023/A:1008678014487]
• 29: T. A. Henzinger , Pei-Hsin Ho , H. Wong-Toi, HYTECH: the next generation, Proceedings of the 16th IEEE Real-Time Systems Symposium, p.56, December 05-07, 1995
• 30: Michael Hind , Anthony Pioli, Evaluating the effectiveness of pointer alias analyses, Science of Computer Programming, v.39 n.1, p.31-55, Jan. 2001 [doi>10.1016/S0167-6423(00)00014-9]
• 31: Gerard J. Holzmann, Software Analysis and Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.1-16, July 27-31, 2002
• 32: Franco Ivanicic , Ilya Shlyakhter , Aarti Gupta , Malay K. Ganai, Model Checking C Programs Using F-SOFT, Proceedings of the 2005 International Conference on Computer Design, p.297-308, October 02-05, 2005 [doi>10.1109/ICCD.2005.77]
• 33: Franjo Ivani , Zijiang Yang , Malay K. Ganai , Aarti Gupta , Pranav Ashar, Efficient SAT-based bounded model checking for software verification, Theoretical Computer Science, v.404 n.3, p.256-274, September, 2008 [doi>10.1016/j.tcs.2008.03.013]
• 34: Ivančić, F., Yang, Z., Shlyakhter, I., Ganai, M., Gupta, A., and Ashar, P. 2005a. F-Soft: Software verification platform. In Proceedings of the Computer-Aided Verification. Lecture Notes on Computer Science, vol. 3576, Springer-Verlag, 301--306.
• 35: Jain, H., Ivančić, F., Gupta, A., and Ganai, M. 2005. Localization and register sharing for predicate abstraction. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes on Computer Science, vol. 3440. Springer-Verlag, 394--409.
• 36: Jayaraman, G., Ranganath, V. P., and Hatcliff, J. 2005. Kaveri: Delivering the indus java program slicer to eclipse. In Proceedings of the Fundamental Approaches to Software Engineering (FASE). 269--272.
• 37: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 38: Antoine Miné, The Octagon Abstract Domain, Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), p.310, October 02-05, 2001
• 39: Amit Narayan , Adrian J. Isles , Jawahar Jain , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Reachability analysis using partitioned-ROBDDs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.388-393, November 09-13, 1997, San Jose, California, United States
• 40: Nelson, G. 1984. Combining satisfiability procedures by equality-sharing. Contemp. Math. 29, 201--211.
• 41: William Pugh, The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing, p.4-13, November 18-22, 1991, Albuquerque, New Mexico, United States [doi>10.1145/125826.125848]
• 42: Quielle, J. P. and Sifakis, J. 1981. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th Annual Symposium on Programming.
• 43: Ranjan, R. K., Aziz, A., Brayton, R. K., Plessier, B. F., and Pixley, C. 1995. Efficient BDD algorithms for FSM synthesis and verification. In Proceedings of the International Workshop on Logic Synthesis (IWLS'95).
• 44: Radu Rugina , Martin Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.182-195, June 18-21, 2000, Vancouver, British Columbia, Canada
• 45: Sankaranarayanan, S., Ivančić, F., and Gupta, A. 2007. Program analysis using symbolic ranges. In Proceedings of the Static Analysis Symposium.
• 46: Sankaranarayanan, S., Ivančić, F., Shlyakhter, I., and Gupta, A. 2006. Static analysis in disjunctive numerical domains. In Proceedings of the Static Analysis Symposium.
• 47: Luc Séméria , Giovanni De Micheli, SpC: synthesis of pointers in C: application of pointer analysis to the behavioral synthesis from C, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.340-346, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289051]
• 48: Somenzi, F. 1995. CUDD: CU Decision Diagram Package. University of Colorado at Boulder, ftp://vlsi.colorado.edu/pub/.
• 49: Tip, F. 1995. A survey of program slicing techniques. J. Program. Lang. 3, 121--189.
• 50: 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
• 51: Wang, C., Yang, Z., Gupta, A., and Ivančić, F. 2006. Whodunit? causal analysis for counterexamples. In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis.
• 52: Chao Wang , Zijiang Yang , Franjo Ivančić , Aarti Gupta, Disjunctive image computation for software verification, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.12 n.2, p.10-es, April 2007 [doi>10.1145/1230800.1230802]
• 53: Yang, Z., Wang, C., Ivančić, F., and Gupta, A. 2006. Mixed symbolic representations for model checking software programs. In ACM/IEEE International Conference on Formal Methods and Models for Codesign (Memocode).
• 54: Yavuz-Kahveci, T., Bartzis, C., and Bultan, T. 2005. Action language verifier, extended. In Proceedings of the Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 3576, Springer-Verlag, 413--416.
• 55: Yavuz-Kahveci, T. and Bultan, T. 2003. A symbolic manipulator for automated verification of reactive systems with heterogeneous data types. Int. J. Softw. Tools Tech. Trans. 5,1, 15--33.
• 56: Tuba Yavuz-Kahveci , Murat Tuncer , Tevfik Bultan, A Library for Composite Symbolic Representations, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.52-66, April 02-06, 2001
• 57: Zaks, A., Yang, Z., Shlyakhter, I., Ivančić, F., Cadambi, S., Ganai, M. K., Gupta, A., and Ashar, P. 2008. Bitwidth reduction via symbolic interval analysis for software model checking. IEEE Trans. Comput. Aid. Des. Integr. Circ. Syst., 27, 8.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Verification

Keywords:
Model checking, binary decision diagram, composite symbolic formula, image computation, presburger arithmetic, reachability analysis