Abstract
In the domain of software verification, predicate abstraction has emerged to be a powerful and popular technique for extracting finite-state models from often complex source code. In this paper, we report on the application of three techniques for improving the performance of the predicate abstraction refinement loop. The first technique allows faster computation of the abstraction. Instead of maintaining a global set of predicates, we find predicates relevant to various basic blocks of the program by weakest pre-condition propagation along spurious program traces. The second technique enables faster model checking of the abstraction by reducing the number of state variables in the abstraction. This is done by re-using Boolean variables to represent different predicates in the abstraction. However, some predicates are useful at many program locations and discovering them lazily in various parts of the program leads to a large number of abstraction refinement iterations. The third technique attempts to identify such predicates early in the abstraction refinement loop and handles them separately by introducing dedicated state variables for such predicates. We have incorporated these techniques into NEC’s software verification tool F-Soft, and present promising experimental results for various case studies using these techniques.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ball, T., Cook, B., Das, S., Rajamani, S.: Refining approximations in software predicate abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 388–403. Springer, Heidelberg (2004)
Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. Programming Language Design and Implementation, 203–213 (2001)
Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 268. Springer, Heidelberg (2001)
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: SPIN Workshop on Model Checking of Software. Springer, Heidelberg (2001)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE 2003, pp. 385–395. IEEE, Los Alamitos (2003)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI–C programs using SAT. Formal Methods in System Design 25, 105–127 (2004)
Cousot, P., Cousot, R.: 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, pp. 238–252 (1977)
Craig, W.: Linear reasoning. Journal of Symbolic Logic 22, 250–268 (1957)
Das, S., Dill, D., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999)
Dijkstra, E.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: CAV 1997, pp. 72–83. Springer, Heidelberg (1997)
Gupta, A., Ganai, M.K., Ashar, P., Yang, Z.: Iterative abstraction using SAT-based BMC with proof analysis. In: International Conference on Computer Aided Design (ICCAD) (2003)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, pp. 58–70 (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL 2004, pp. 232–244. ACM Press, New York (2004)
Ivančić, F., Yang, Z., Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. In: Symposium on Leveraging Applications of Formal Methods (2004)
Jain, H., Kroening, D., Clarke, E.: Verification of SpecC using predicate abstraction. In: MEMOCODE 2004, pp. 7–16. IEEE, Los Alamitos (2004)
Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 141–153. Springer, Heidelberg (2003)
Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Rugina, R., Rinard, M.C.: Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In: PLDI 2000, pp. 182–195 (2000)
Rusu, V., Singerman, E.: On proving safety properties by integrating static analysis, theorem proving and abstraction. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 178–192. Springer, Heidelberg (1999)
Zaks, A., Ivančić, F., Cadambi, H., Shlyakhter, I., Yang, Z., Ganai, M., Gupta, A., Ashar, P.: Range analysis for software verification (2005) (Submitted for publication)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jain, H., Ivančić, F., Gupta, A., Ganai, M.K. (2005). Localization and Register Sharing for Predicate Abstraction. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)