Disjunctive image computation for software verification

ABSTRACT

Existing BDD-based symbolic algorithms designed for hardware designs do not perform well on software programs. We propose novel techniques based on unique characteristics of software programs. Our algorithm divides an image computation step into a disjunctive set of easier ones that can be performed in isolation. We use hypergraph partitioning to minimize the number of live variables in each disjunctive component, and variable scopes to simplify transition relations and reachable state subsets. Our experiments on nontrivial C programs show that BDD-based symbolic algorithms can directly handle software models with a much larger number of state variables than for hardware designs.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: Rajeev Alur , Costas Courcoubetis , David Dill, Model-checking in dense real-time, Information and Computation, v.104 n.1, p.2-34, May 1993 [doi>10.1006/inco.1993.1024]
• 3: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 4: 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
• 5: Barner, S. and Rabinovitz, I. 2003. Efficient symbolic model checking of software using partial disjunctive partitioning. In Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME). Lecture Notes in Computer Science, vol. 2860. Springer Verlag, Berlin.
• 6: Ahmed Bouajjani , Javier Esparza , Oded Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking, Proceedings of the 8th International Conference on Concurrency Theory, p.135-150, July 01-04, 1997
• 7: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 8: M. C. Browne , E. M. Clarke , O. Grumberg, Reasoning about networks with many identical finite state processes, Information and Computation, v.81 n.1, p.13-31, April 1989 [doi>10.1016/0890-5401(89)90026-6]
• 9: 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]
• 10: 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]
• 11: Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. 1990. Symbolic model checking: 10²⁰ states and beyond. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA. 1--33.
• 12: 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]
• 13: Pankaj Chauhan , Edmund M. Clarke , Somesh Jha , Jim Kukula , Tom Shiple , Helmut Veith , Dong Wang, Non-linear quantification scheduling in image computation, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 14: Cho, H., Hachtel, G. D., Macii, E., Poncino, M., and Somenzi, F. 1996. Automatic state space decomposition for approximate FSM traversal based on circuit analysis. IEEE Trans. Comput. Aided Des. 15, 12 (Dec.), 1451--1464.
• 15: Clarke, E., Grumberg, O., and Peled, D. 2000. Model checking. MIT Press, Cambridge, MA.
• 16: Clarke, E., Kroening, D., and Lerda, F. 2004. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, K. Jensen and A. Podelski, eds. Lecture Notes in Computer Science, vol. 2988. Springer Verlag, Berlin. 168--176.
• 17: 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
• 18: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 19: Cook, B., Kroening, D., and Sharygina, N. 2005. Symbolic model checking for asynchronous Boolean programs. In Proceedings of the 12th International SPIN Workshop on Model Checking of Software. 75--90.
• 20: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 21: Olivier Coudert , Christian Berthet , Jean Christophe Madre, Verification of Synchronous Sequential Machines Based on Symbolic Execution, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, p.365-373, June 12-14, 1989
• 22: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 23: Edwards, S., Ma, T., and Damiano, R. 2001. Using a hardware model checker to verify software. In Proceedings of the 4th International Conference on ASIC (ASICON). IEEE, Los Alamitos, CA.
• 24: 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
• 25: 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]
• 26: 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]
• 27: Gerard J. Holzmann , Doron Peled, An improvement in formal verification, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, p.197-211, January 1995
• 28: Ivančić, F., Yang, Z., Gupta, A., Ganai, M., and Ashar, P. 2004. Efficient SAT-based bounded model checking for software verification. In 1st International Symposium on Leveraging Applications of Formal Methods.
• 29: Ivančić, F., Yang, Z., Shlyakhter, I., Ganai, M., Gupta, A., and Ashar, P. 2005. F-Soft: Software verification platform. In Proceedings of the Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 3576. Springer Verlag, Berlin. 301--306.
• 30: HoonSang Jin , Andreas Kuehlmann , Fabio Somenzi, Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.312-326, April 08-12, 2002
• 31: HoonSang Jin , Kavita Ravi , Fabio Somenzi, Fate and Free Will in Error Traces, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.445-459, April 08-12, 2002
• 32: Karypis, G. and Kumar, V. 1998. Multilevel algorithms for multi-constraint graph partitioning. Tech. Rep. 98-019, University of Minnesota, Department of Computer Science. May.
• 33: Orna Kupferman , Moshe Y. Vardi, Model Checking of Safety Properties, Formal Methods in System Design, v.19 n.3, p.291-314, November 2001 [doi>10.1023/A:1011254632723]
• 34: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 35: In-Ho Moon , Gary D. Hachtel , Fabio Somenzi, Border-Block Triangular Form and Conjunction Schedule in Image Computation, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.73-90, November 01-03, 2000
• 36: 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
• 37: Quielle, J. P. and Sifakis, J. 1981. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th Annual Symposium on Programming.
• 38: Ranjan, R. K., Aziz, A., Brayton, R. K., Plessier, B. F., and Pixley, C. 1995. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS (Lake Tahoe, CA).
• 39: Mooly Sagiv , Thomas Reps , Susan Horwitz, Precise interprocedural dataflow analysis with applications to constant propagation, Theoretical Computer Science, v.167 n.1-2, p.131-170, Oct. 30, 1996
• 40: 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
• 41: 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]
• 42: 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
• 43: Chao Wang , Gary D. Hachtel , Fabio Somenzi, The Compositional Far Side of Image Computation, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.334, November 09-13, 2003 [doi>10.1109/ICCAD.2003.140]
• 44: Chao Wang , Zijiang Yang , Franjo Ivančić , Aarti Gupta, Disjunctive image computation for embedded software verification, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 45: Pierre Wolper , Denis Leroy, Reliable Hashing without Collosion Detection, Proceedings of the 5th International Conference on Computer Aided Verification, p.59-70, June 28-July 01, 1993
• 46: Zaks, A., Shlyakhter, I., Ivančić, F., Cadambi, H., Yang, Z., Ganai, M., Gupta, A., and Ashar, P. 2006. Range analysis for software verification. In 4th International Workshop on Software Verification and Validation (SVV).

INDEX TERMS

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

General Terms:
Algorithms, Verification

Keywords:
Model checking, binary decision diagram, formal verification, image computation, reachability analysis