×

Efficient SAT-based bounded model checking for software verification. (English) Zbl 1293.68079

Summary: This paper discusses our methodology for formal analysis and automatic verification of software programs. It is applicable to a large subset of the C programming language that includes pointer arithmetic and bounded recursion. We consider reachability properties, in particular whether certain assertions or basic blocks are reachable in the source code, or whether certain standard property violations can occur. We perform this analysis via a translation to a Boolean circuit representation based on modeling basic blocks. The program is then analyzed by a back-end SAT-based bounded model checker, where each unrolling is mapped to one step in a block-wise execution of the program.
The main contributions of this paper are as follows: (1) Use of basic block-based unrollings with SAT-based bounded model checking of software programs. This allows us to take advantage of SAT-based learning inherent to the best performing bounded model checkers. (2) Various heuristics customized for models automatically generated from software, allowing a more efficient SAT-based analysis. (3) A prototype tool called F-Soft has been implemented using our methodology.
We present experimental results based on multiple case studies including a C-based implementation of a network protocol, and compare the performance gains using the proposed heuristics.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] Alur, R.; Courcoubetis, C.; Dill, D.L., Model-checking in dense real-time, Information and computation, 104, 1, 2-34, (1993) · Zbl 0783.68076
[2] R. Alur, L. deAlfaro, R. Grosu, T.A. Henzinger, M. Kang, R. Majumdar, F. Mang, C.M. Kirsch, B.Y. Wang, MOCHA: A model checking tool that exploits design structure, in: Intern. Conf. on Software Engineering, 2001, pp. 835-836
[3] R. Alur, B.-Y. Wang, Verifying network protocol implementations by symbolic refinement checking, in: 13th Conference on Computer Aided Verification, 2001, pp. 169-181 · Zbl 0991.68546
[4] T. Ball, R. Majumdar, T.D. Millstein, S.K. Rajamani, Automatic predicate abstraction of C programs, in: ACM SIGPLAN Conference on Programming Language Design and Implementation, 2001, pp. 203-213
[5] Ball, T.; Rajamani, S., Bebop: A symbolic model checker for Boolean programs, (), 113-130 · Zbl 0976.68540
[6] A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, in: Proceedings of the 36th ACM/IEEE Design Automation Conference, 1999, pp. 317-320
[7] Blanchet, B.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X., (), 196-207
[8] Boujjani, A.; Esparza, J.; Maler, O., Reachability analysis of pushdown automata: applications to model checking, (), 135-150
[9] Browne, M.; Clarke, E.M.; Grumberg, O., Reasoning about networks with many identical finite state processes, Information and computation, 81, 13-31, (1989) · Zbl 0709.68610
[10] Bryant, R.E., Graph-based algorithms for Boolean-function manipulation, IEEE transactions on computers, C(35), 677-691, (1986) · Zbl 0593.94022
[11] Chauhan, P.; Clarke, E.M.; Kukula, J.; Sapra, S.; Veith, H.; Wang, D., Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis, (), 33-51 · Zbl 1019.68618
[12] Clarisó, R.; Cortadella, J., The octahedron abstract domain, (), 312-327 · Zbl 1104.68410
[13] Clarke, E.M.; Fujita, M.; Rajan, S.P.; Reps, T.; Shankar, S.; Teitelbaum, T., Programs slicing for VHDL, International journal on software tools for technology transfer (STTT), 4, 1, 125-137, (2002)
[14] Clarke, E.M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement, Computer aided verification, 154-169, (2000) · Zbl 0974.68517
[15] Clarke, E.M.; Grumberg, O.; Peled, D.A., Model checking, (2000), MIT Press
[16] Clarke, E.M.; Kroening, D.; Lerda, F., A tool for checking ANSI-C programs, (), 168-176 · Zbl 1126.68470
[17] E.M. Clarke, D. Kroening, N. Sharygina, K. Yorav, Predicate abstraction of ANSI-C programs using SAT, in: Model Checking for Dependable Software-Intensive Systems Workshop, 2003 · Zbl 1090.68022
[18] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S. Păsăreanu, Robby, H. Zheng, Bandera: Extracting finite-state models from Java source code, in: International Conference on Software Engineering, 2000, pp. 439-448
[19] Cousot and, P; Cousot, R, Static determination of dynamic properties of programs, (), 106-130
[20] P. Cousot, R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, 1977, pp. 238-252
[21] P. Cousot, N. Halbwachs, Automatic discovery of linear restraints among the variables of a program, in: ACM POPL, January 1978, pp. 84-97
[22] Das, S.; Dill, D.; Park, S., Experience with predicate abstraction, (), 160-171 · Zbl 1046.68589
[23] Dor, N.; Rodeh, M.; Sagiv, M., CSSV: towards a realistic tool for statically detecting all buffer overflows in C, ()
[24] Fernandez, J.; Garavel, H.; Kerbrat, A.; Mateescu, R.; Mounier, L.; Sighireanu, M., CADP: A protocol validation and verification toolbox, ()
[25] Ganai, M.K.; Gupta, A.; Ashar, P., Efficient memory modeling for SAT-based BMC, ()
[26] Ganai, M.K.; Gupta, A.; Ashar, P., Diver: SAT-based model checking platform for verifying large scale systems, () · Zbl 1087.68588
[27] Godefroid, P., Verisoft: A tool for the automatic analysis of concurrent reactive software, ()
[28] E. Goldberg, Y. Novikov, Verification of proofs of unsatisfiability for CNF formulas, in: Conference on Design Automation and Test in Europe, 2003
[29] Goubault, E.; Putot, S., Static analysis of numerical algorithms, (), 18-34 · Zbl 1225.68073
[30] Graf, S.; Saidi, H., Construction of abstract state graphs with PVS, (), 72-83
[31] Gupta, A.; Ganai, M.K.; Wang, C.; Yang, Z.; Ashar, P., Abstraction and BDDs complement SAT-based BMC in diver, (), 206-209
[32] A. Gupta, M.K. Ganai, Z. Yang, P. Ashar, Iterative abstraction using SAT-based BMC with proof analysis, in: Intern. Conf. on Computer Aided Design, November 2003, pp. 416-423
[33] Gupta, A.; Yang, Z.; Ashar, P.; Gupta, A., SAT-based image computation with applications in reachability analysis, (), 354-371
[34] Havelund, K.; Pressburger, T., Model checking Java programs using Java pathfinder, Software tools for technology transfer, 2, 4, (2000) · Zbl 1059.68585
[35] Henzinger, T.A.; Jhala, R.; Majumdar, R.; McMillan, K., Abstractions from proofs, (), 232-244 · Zbl 1325.68147
[36] M. Hind, Pointer analysis: Haven’t we solved this problem yet?, in: 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE’01, June 2001
[37] Holzmann, G.J., The model checker SPIN, IEEE transactions on software engineering, 23, 5, 279-295, (1997)
[38] Ivančić, F.; Shlyakhter, I.; Gupta, A.; Ganai, M.K.; Kahlon, V.; Wang, C.; Yang, Z., Model checking C programs with F-SOFT, ()
[39] F. Ivančić, Z. Yang, M. Ganai, A. Gupta, P. Ashar, Efficient SAT-based bounded model checking for software verification, in: Symposium on Leveraging Formal Methods in Applications, ISoLA, 2004 · Zbl 1293.68079
[40] Ivančić, F.; Yang, Z.; Shlyakhter, I.; Ganai, M.K.; Gupta, A.; Ashar, P., F-SOFT: software verification platform, () · Zbl 1081.68581
[41] Jain, H.; Ivančić, F.; Gupta, A.; Ganai, M.K., Localization and register sharing for predicate abstraction, (), 397-412 · Zbl 1087.68593
[42] Jain, H.; Ivančić, F.; Gupta, A.; Shlyakhter, I.; Wang, C., Using statically computed invariants inside the predicate abstraction and refinement loop, (), 137-151
[43] Karr, M., Affine relationships among variables of a program, Acta informatica, 6, 133-151, (1976) · Zbl 0358.68025
[44] Krinke, J., Context-sensitive slicing of concurrent programs, (), 178-187
[45] Kroening, D.; Clarke, E.M.; Yorav, K., Behavioral consistency of C and verilog programs using bounded model checking, (), 368-371
[46] Kurshan, R.P., Computer-aided verification of co-ordinating processes: the automata theoretic approach, (1994), Princeton University Press
[47] Lahiri, S.K.; Bryant, R.E.; Cook, B., A symbolic approach to predicate abstraction, () · Zbl 1278.68181
[48] Marques-Silva, J.P.; Sakallah, K.A., GRASP: A search algorithm for propositional satisfiability, IEEE transactions on computers, 48, 5, 506-521, (1999) · Zbl 1392.68388
[49] McMillan, K.L., Symbolic model checking: an approach to the state explosion problem, (1993), Kluwer Academic Publishers
[50] McMillan, K.L., Applying SAT methods in unbounded symbolic model checking, () · Zbl 1010.68509
[51] McMillan, K.L., Interpolation and SAT-based model checking, (), 1-13 · Zbl 1278.68184
[52] McMillan, K.L.; Amla, N., Automatic abstraction without counterexamples, (), 2-17 · Zbl 1031.68520
[53] Miné, A., A new numerical abstract domain based on difference-bound matrices, (), 155-172 · Zbl 0984.68034
[54] Miné, A, The octagon abstract domain, (), 310-319
[55] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an efficient SAT solver, in: Design Automation Conference, 2001
[56] Prasad, M.R.; Biere, A.; Gupta, A., A survey of recent advances in SAT-based formal verification, Software tools for technology transfer (STTT), 7, 2, 156-173, (2005)
[57] Robby; Dwyer, M.B.; Hatcliff, J., Bogor: an extensible and highly-modular software model checking framework, (), 267-276
[58] Rugina, R.; Rinard, M.C., Symbolic bounds analysis of pointers, array indices, and accessed memory regions, (), 182-195
[59] Sankaranarayanan, S.; Colón, M.; Sipma, H.B.; Manna, Z., Efficient strongly relational polyhedral analysis, () · Zbl 1176.68051
[60] Sankaranarayanan, S.; Ivančić, F.; Gupta, A., Program analysis using symbolic ranges, (), 366-383 · Zbl 1211.68101
[61] Sankaranarayanan, S.; Ivančić, F.; Shlyahkter, I.; Gupta, A., Static analysis in disjunctive numerical domains, (), 3-17 · Zbl 1225.68077
[62] Séméria, L.; deMicheli, G., Spc: synthesis of pointers in C, application of pointer analysis to the behavioral synthesis from C, (), 321-326
[63] Sheeran, M.; Singh, S.; Stalmarck, G., Checking safety properties using induction and a SAT solver, (), 108-125
[64] W. Simpson, PPP: The point-to-point protocol, RFC 1661, IETF, June 1994
[65] SystemC
[66] Tip, F., A survey of program slicing techniques, Journal of programming languages, 3, 121-189, (1995)
[67] W. Visser, K. Havelund, G. Brat, S. Park, Model checking programs, in: Proceedings of the 15th IEEE International Conference on Automated Software Engineering, 2000
[68] Wagner, D.; Foster, J.; Brewer, E.; Aiken, A., A first step towards automated detection of buffer overrun vulnerabilities, (), 3-17
[69] Wang, C.; Yang, Z.; Ivančić, F.; Gupta, A., Disjunctive image computation for embedded software verification, (), 1205-1210
[70] Yang, Z.; Wang, C.; Gupta, A.; Ivančić, F., Mixed symbolic representations for model checking software programs, (), 17-26
[71] A. Zaks, S. Cadambi, I. Shlyakhter, F. Ivančić, Z. Yang, M.K. Ganai, A. Gupta, P. Ashar, Range analysis for software verification, in: International Workshop on Software Verification and Validation, SVV, August 2006
[72] L. Zhang, S. Malik, Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications, in: Conference on Design Automation and Test in Europe, 2003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.