Disjunctive image computation for embedded software verification

ABSTRACT

Finite state models generated from software programs have unique characteristics that are not exploited by existing model checking algorithms. In this paper, we propose a novel disjunctive image computation algorithm and other simplifications based on these characteristics. Our algorithm divides an image computation into a disjunctive set of easier ones that can be performed in isolation. Hypergraph partitioning is used to minimize the number of live variables in each disjunctive component. We use the live variables to simplify transition relations and reachable state subsets. Our experiments on a set of real-world C programs show that the new algorithm achieves orders-of-magnitude performance improvement over the best known conjunctive image computation algorithm.

REFERENCES

• 1: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 2: 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
• 3: R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pix-ley. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS95, May 1995.
• 4: 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
• 5: 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]
• 6: 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
• 7: 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]
• 8: 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
• 9: 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]
• 10: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 11: S. Edwards, T. Ma, and R. Damiano. Using a hardware model checker to verify software. Presented at Int. Conf. on ASIC, 2001.
• 12: 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
• 13: S. Barner and I. Rabinovitz. Efficient symbolic model checking of software using partial disjunctive partitioning. In Correct Hardware Design and Verification Methods (CHARME'03), pages 35--50. LNCS 2860.
• 14: F. Ivančić, Z. Yang, I. Shlyakhter, M. Ganai, A. Gupta, and P. Ashar. F-SOFT: Software verification platform. In Computer-Aided Verification, pages 301--306, 2005. LNCS 3576.
• 15: 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]
• 16: H. Cho, G. D. Hachtel, E. Macii, M. Poncino, and F. Somenzi. Automatic state space decomposition for approximate FSM traversal based on circuit analysis. IEEE Trans. on CAD, 15(12):1451--1464, 1996.
• 17: G. Karypis and V. Kumar. Multilevel algorithms for multi-constraint graph partitioning. Technical Report 98-019, University of Minnesota, 1998.