Complexity and algorithms for monomial and clausal predicate abstraction. (English) Zbl 1250.68194
Schmidt, Renate A. (ed.), Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02958-5/pbk). Lecture Notes in Computer Science 5663. Lecture Notes in Artificial Intelligence, 214-229 (2009).
Summary: In this paper, we investigate the asymptotic complexity of various predicate abstraction problems relative to the asymptotic complexity of checking an annotated program in a given assertion logic. Unlike previous approaches, we pose the predicate abstraction problem as a decision problem, instead of the traditional inference problem. For assertion logics closed under weakest (liberal) precondition and Boolean connectives, we show two restrictions of the predicate abstraction problem where the two complexities match. The restrictions correspond to the case of monomial and clausal abstraction. For these restrictions, we show a symbolic encoding that reduces the predicate abstraction problem to checking the satisfiability of a single formula whose size is polynomial in the size of the program and the set of predicates. We also provide a new iterative algorithm for solving the clausal abstraction problem that can be seen as the dual of the Houdini algorithm for solving the monomial abstraction problem.
For the entire collection see [Zbl 1167.68006].
For the entire collection see [Zbl 1167.68006].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B35 | Mechanization of proofs and logical operations |
| 68Q25 | Analysis of algorithms and problem complexity |
References:
| [1] | Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Programming Language Design and Implementation (PLDI 2001), pp. 203–213 (2001) · doi:10.1145/378795.378846 |
| [2] | Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Program Analysis For Software Tools and Engineering (PASTE 2005), pp. 82–87 (2005) · doi:10.1145/1108792.1108813 |
| [3] | Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000) · Zbl 0974.68517 · doi:10.1007/10722167_15 |
| [4] | Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: Principles of Programming Languages (POPL 2009), pp. 302–314 (2009) · Zbl 1315.68086 · doi:10.1145/1594834.1480921 |
| [5] | Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL 1977), pp. 238–252 (1977) · doi:10.1145/512950.512973 |
| [6] | Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages (POPL 1978), pp. 84–96 (1978) · doi:10.1145/512760.512770 |
| [7] | Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001) · Zbl 0977.68671 · doi:10.1007/3-540-45251-6_29 |
| [8] | Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997) · doi:10.1007/3-540-63166-6_10 |
| [9] | Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 120–135. Springer, Heidelberg (2009) · Zbl 1206.68087 · doi:10.1007/978-3-540-93900-9_13 |
| [10] | Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Principles of Programming Languages (POPL), pp. 232–244 (2004) · Zbl 1325.68147 · doi:10.1145/964001.964021 |
| [11] | Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Principles of Programming Languages (POPL 2002), pp. 58–70 (2002) · Zbl 1323.68374 · doi:10.1145/503272.503279 |
| [12] | Jain, H., Kroening, D., Sharygina, N., Clarke, E.M.: Word level predicate abstraction and refinement for verifying rtl verilog. In: Design Automation Conference (DAC 2005), pp. 445–450. ACM, New York (2005) · doi:10.1145/1065579.1065697 |
| [13] | Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1995) · Zbl 0822.68116 · doi:10.1515/9781400864041 |
| [14] | Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267–281. Springer, Heidelberg (2004) · Zbl 1202.68251 · doi:10.1007/978-3-540-24622-0_22 |
| [15] | Lahiri, S.K., Qadeer, S.: Back to the future: Revisiting precise program verification using SMT solvers. In: Principles of Programming Languages (POPL 2008), pp. 171–182 (2008) · Zbl 1295.68087 · doi:10.1145/1328438.1328461 |
| [16] | Lahiri, S.K., Qadeer, S., Galeotti, J.P., Voung, J.W., Wies, T.: Intra-module inference. In: Computer-Aided Verification (CAV 2009) (July 2009) · doi:10.1007/978-3-642-02658-4_37 |
| [17] | Sagiv, S., Reps, T.W., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems (TOPLAS) 20(1), 1–50 (1998) · doi:10.1145/271510.271517 |
| [18] | Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 53–68. Springer, Heidelberg (2004) · Zbl 1104.68023 · doi:10.1007/978-3-540-27864-1_7 |
| [19] | Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005) · Zbl 1111.68514 · doi:10.1007/978-3-540-30579-8_2 |
| [20] | Satisfiability Modulo Theories Library (SMT-LIB), http://goedel.cs.uiowa.edu/smtlib/ |
| [21] | Solar-Lezama, A., Rabbah, R.M., Bodík, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Programming Language Design and Implementation (PLDI 2005), pp. 281–294. ACM, New York (2005) |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
