Interpolation Systems for Ground Proofs in Automated Deduction: a Survey

详细信息    查看全文

• 作者：Maria Paola Bonacina (1)
  Moa Johansson (2)
  
  1. Dipartimento di Informatica ; Universit脿 degli Studi di Verona ; Strada Le Grazie 15 ; 37134 ; Verona ; Italy
  2. Department of Computer Science ; Chalmers University of Technology ; G枚teborg ; Sweden
  
• 关键词：Interpolation systems ; Satisfiability modulo theories ; Decision procedures ; Theory combination
• 刊名：Journal of Automated Reasoning
• 出版年：2015
• 出版时间：April 2015
• 年：2015
• 卷：54
• 期：4
• 页码：353-390
• 全文大小：972 KB
• 参考文献：1. Albarghouthi, A, McMillan, KL Beautiful interpolants. In: ditors">Sharygina, N, Veith, H eds. (2013) Proceedings of the 25th Conference on Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science. Springer, Berlin, pp. 313-329
  2. Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bj酶rner N, Voronkov, A (eds.) Proceedings of the 18th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 7180 of Lecture Notes in Artificial Intelligence, pp. 46鈥?1. Springer, Berlin (2012)
  3. Armando, A, Bonacina, MP, Ranise, S, Schulz, S (2009) New results on rewrite-based satisfiability procedures. ACM Trans Comput Log 10: pp. 129-179 CrossRef
  4. Armando, A, Ranise, S, Rusinowitch, M (2003) A rewriting approach to satisfiability procedures. Inf Comput 183: pp. 140-164 CrossRef
  5. Barrett, CW, Dill, DL, Stump, A Checking satisfiability of first-order formulas by incremental translation to SAT. In: ditors">Larsen, KG, Brinksma, E eds. (2002) Proceedings of the 14th Conference on Computer Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science. Springer, Berlin, pp. 236-249
  6. Barrett, CW, Dill, DL, Stump, A A generalization of Shostak鈥檚 method for combining decision procedures. In: ditors">Armando, A eds. (2002) Proceedings of the 4th Workshop on Frontiers of Combining Systems (FroCoS), volume 2309 of Lecture Notes in Computer Science. Springer, Berlin
  7. Beyer, D, Zufferey, D, Majumdar, R CSIsat: interpolation for LA+EUF. In: ditors">Gupta, A, Malik, S eds. (2008) Proceedings of the 20th Conference on Computer Aided Verification (CAV), volume 5123 of Lecture Notes in Computer Science. Springer, Berlin, pp. 304-308
  8. Bonacina, MP On theorem proving for program checking 鈥?historical perspective and recent developments. In: ditors">Fernandez, M eds. (2010) Proceedings of the 12th International Symposium on Principles and Practice of Declarative Programming (PPDP). ACM, New York, pp. 1-11
  9. Bonacina, MP, Dershowitz, N (2007) Abstract canonical inference. ACM Trans. Comput. Log. 8: pp. 180-208 CrossRef
  10. Bonacina, MP, Echenim, M Rewrite-based satisfiability procedures for recursive data structures. In: ditors">Cook, B, Sebastiani, R eds. (2007) Proceedings of the 4th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006), volume 174(8) of Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam, pp. 55-70
  11. Bonacina, MP, Echenim, M (2008) On variable-inactivity and polynomial $\mathcal {T}$T-satisfiability procedures. J. Log. Comput. 18: pp. 77-96 CrossRef
  12. Bonacina, MP, Hsiang, J (1998) On the modelling of search in theorem proving 鈥?towards a theory of strategy analysis. Inf. Comput. 147: pp. 171-208 CrossRef
  13. Bonacina, MP, Johansson, M On interpolation in decision procedures. In: ditors">Br眉nnler, K, Metcalfe, G eds. (2011) Proceedings of the 20th International Conference on Analytic Tableaux and Related Methods (TABLEAUX), volume 6793 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 1-16
  14. Bonacina, MP, Johansson, M Towards interpolation in an SMT solver with integrated superposition. In: ditors">Lahiri, S, Seshia, S A eds. (2011) Notes of the 9th International Workshop on Satisfiability Modulo Theories (SMT), number UCB/EECS-2011-80 in Technical Reports. Department of EECS, University of California at Berkeley, Berkeley, pp. 9-18
  15. Bonacina, MP, Johansson, M (2015) On interpolation in automated theorem proving. J. Autom. Reason. 54: pp. 69-97 CrossRef
  16. Bradley, AR, Manna, Z (2007) The calculus of computation 鈥?decision procedures with applications to verification. Springer, Berlin
  17. Brillout, A, Kroening, D, R眉mmer, P, Wahl, T An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: ditors">Giesl, J, H盲hnle, R eds. (2010) Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 384-399
  18. Brillout, A., Kroening, D., R眉mmer, P., Wahl, T.: Program verification via Craig interpolation for Presburger arithmetic with arrays. Notes of the 6th International Verification Workshop (VERIFY), 2010. Available at http://www.philipp.ruemmer.org/
  19. Brillout, A, Kroening, D, R眉mmer, P, Wahl, T Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In: ditors">Jhala, R, Schmidt, D eds. (2011) Proceedings of the 12th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), volume 6538 of Lecture Notes in Computer Science. Springer, Berlin, pp. 88-102
  20. Bruttomesso, R, Ghilardi, S, Ranise, S A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints. In: ditors">Tinelli, C, Sofronie-Stokkermans, V eds. (2011) Proceedings of the 8th Symposium on Frontiers of Combining Systems (FroCoS), volume 6989 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 103-118
  21. Bruttomesso, R, Ghilardi, S, Ranise, S From strong amalgamability to modularity of quantifier-free interpolation. In: ditors">Gramlich, B, Miller, D, Sattler, U eds. (2012) Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), volume 7364 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 118-133
  22. Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation for a theory of arrays. Logical Methods Comput. Sci. 8(2) (2012)
  23. Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1) (2014)
  24. Bruttomesso, R, Rollini, SF, Sharygina, N, Tsitovich, A (2010) Flexible interpolation generation in satisfiability modulo theories. In: Proceedings of the 14th International Conference on Computer-Aided Design (ICCAD). IEEE, Los Alamitos
  25. Christ, J., Hoenicke, J.: Instantiation-based interpolation for quantified formulae. Notes of the 8th International Workshop on Satisfiability Modulo Theories (SMT) (2010)
  26. Cimatti, A, Griggio, A, Sebastiani, R (2010) Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12: pp. Article 7 CrossRef
  27. Cook, SA, Reckhow, RA (1979) The relative efficiency of propositional proof systems. J. Symb. Log. 44: pp. 36-50 CrossRef
  28. Craig, W (1957) Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22: pp. 250-268 CrossRef
  29. Davis, M, Logemann, G, Loveland, D (1962) A machine program for theorem-proving. Comm. ACM 5: pp. 394-397 CrossRef
  30. Davis, M, Putnam, H (1960) A computing procedure for quantification theory. J. ACM 7: pp. 201-215 CrossRef
  31. de Moura, L, Bj酶rner, N Efficient E-matching for SMT-solvers. In: ditors">Pfenning, F eds. (2007) Proceedings of the 21st Conference on Automated Deduction (CADE), volume 4603 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 183-198
  32. de Moura, L, Bj酶rner, N Bugs, moles and skeletons: Symbolic reasoning for software development. In: ditors">Giesl, J, H盲hnle, R eds. (2010) Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 400-411
  33. de Moura, L, Bj酶rner, N (2011) Satisfiability modulo theories: introduction and applications. Comm. ACM 54: pp. 69-77 CrossRef
  34. Dershowitz, N, Plaisted, DA Rewriting. In: ditors">Robinson, A, Voronkov, A eds. (2001) Handbook of automated reasoning, vol. 1. Elsevier, Amsterdam, pp. 535-610 CrossRef
  35. Detlefs, DL, Nelson, G, Saxe, JB (2005) Simplify: a theorem prover for program checking. J. ACM 52: pp. 365-473 CrossRef
  36. D鈥橲ilva, V Propositional interpolation and abstract interpretation. In: ditors">Gordon, AD eds. (2010) Proceedings of the 19th European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science. Springer, Berlin, pp. 185-204
  37. D鈥橲ilva, V, Kroening, D, Purandare, M, Weissenbacher, G Interpolant strength. In: ditors">Barthe, G, Hermenegildo, MV eds. (2010) Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 5944 of Lecture Notes in Computer Science. Springer, Berlin, pp. 129-145
  38. Fitting, M (1996) First-order logic and automated theorem proving. Springer, Berlin CrossRef
  39. Fuchs, A., Goel, A., Grundy, J., Krsti膰, S., Tinelli, C.: Ground interpolation for the theory of equality. Logical Methods Comput. Sci. 8(1) (2012)
  40. Gallier, J (1987) Logic for computer science 鈥?foundations of automatic theorem proving. Wiley, New York
  41. Ganzinger, H, Sofronie-Stokkermans, V, Waldmann, U (2006) Modular proof systems for partial functions with Evans equality. Inf. Comput. 240: pp. 1453-1492 CrossRef
  42. Ge, Y, Barrett, C, Tinelli, C Solving quantified verification conditions using satisfiability modulo theories. In: ditors">Pfenning, F eds. (2007) Proceedings of the 21st conference on automated deduction (CADE), volume 4603 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 167-182
  43. Ge, Y, de Moura, L Complete instantiation for quantified formulas in satisfiability modulo theories. In: ditors">Bouajjani, A, Maler, O eds. (2009) Proceedings of the 21st conference on computer aided verification (CAV), volume 5643 of Lecture Notes in Computer Science. Springer, Berlin, pp. 306-320
  44. Givan, R., McAllester, D.: Proceedings of the 3rd international conference on principles of knowledge representation and reasoning (KR). In: Nebel, B., Rich, C., Swartout, W. R. (eds.) , pp. 403鈥?12. Morgan Kaufmann (1992)
  45. Goel, A, Krsti膰, S, Tinelli, C Ground interpolation for combined theories. In: ditors">Schmidt, R eds. (2009) Proceedings of the 22nd Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 183-198
  46. Griggio, A Effective word-level interpolation for software verification. In: ditors">Bjesse, P, Slobodova, A eds. (2011) Proceedings of the 11th Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE, New York
  47. Gupta, A, Popeea, C, Rybalchenko, A Solving recursion-free Horn clauses over LI+UIF. In: ditors">Yang, H eds. (2011) Proceedings of the 9th Asian Symposium on Programming Languages and Systems (APLAS), volume 7078 of Lecture Notes in Computer Science. Springer, Berlin
  48. Henzinger, TA, Jhala, R, Majumdar, R, McMillan, KL Abstractions from proofs. In: ditors">Leroy, X eds. (2004) Proceedings of the 31st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, New York, pp. 232-244 CrossRef
  49. Hoder, K, Kov脿cs, L, Voronkov, A Interpolation and symbol elimination in Vampire. In: ditors">Giesl, J, H盲hnle, R eds. (2010) Proceedings of the 5th international joint conference on automated reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 188-195
  50. Hoder, K, Kov脿cs, L, Voronkov, A Playing in the grey area of proofs. In: ditors">Hicks, M eds. (2012) Proceedings of the 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, New York, pp. 259-272
  51. Huang, G Constructing Craig interpolation formulas. In: ditors">Du, D-Z, Li, M eds. (1995) Proceedings of the 1st annual international conference on computing and combinatorics (COCOON), volume 959 of Lecture Notes in Computer Science. Springer, Berlin, pp. 181-190
  52. Jain, H.: Verification using satisfiability checking, predicate abstraction and Craig interpolation. PhD thesis, School of Computer Science, Carnegie Mellon University (2008)
  53. Kapur, D., Majumdar, R., Zarba, C.G., et al.: Interpolation for data structures. In: Devambu, P. (ed.) Proceedings of the 14th ACM SIGSOFT Symposium on the Foundations of Software Engineering. ACM Press (2006)
  54. Kleene, SC (1967) Mathematical logic. Wiley Interscience, New York
  55. Kov脿cs, L, Voronkov, A Interpolation and symbol elimination. In: ditors">Schmidt, R eds. (2009) Proceedings of the 22nd Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 199-213
  56. Kraj铆膷ek, J (1997) Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62: pp. 457-486 CrossRef
  57. Kraj铆膷ek, J, Pudl脿k, P (1998) Some consequences of cryptographical conjectures for ${s^{1}_{2}}$s21 and EF. Inf. Comput. 140: pp. 82-94 CrossRef
  58. Kroening, D, Weissenbacher, G Lifting propositional interpolants to the word-level. In: ditors">Baumgartner, J, Sheeran, M eds. (2007) Proceedings of the 7th conference on formal methods in computer aided design (FMCAD). ACM and IEEE, New York, pp. 85-89 CrossRef
  59. Kroening, D, Weissenbacher, G Interpolation-based software verification with Wolverine. In: ditors">Gopalakrishnan, G, Qaader, S eds. (2011) Proceedings of the 23rd conference on computer aided verification (CAV), volume 6806 of Lecture Notes in Computer Science. Springer, Berlin, pp. 573-578
  60. Ludwig, M, Waldmann, U An extension of the Knuth-Bendix ordering with LPO-like properties. In: ditors">Dershowitz, N, Voronkov, A eds. (2007) Proceedings of the 14th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 4790 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 348-362
  61. Malik, S, Zhang, L (2009) Boolean satisfiability: from theoretical hardness to practical success. Comm. ACM 52: pp. 76-82 CrossRef
  62. Marques-Silva, J.P., Sakallah, K.A.: GRASP: A new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE/ACM International Conference on Computer Aided Design (ICCAD), pp. 220鈥?27 (1997)
  63. McAllester, D (1993) Automatic recognition of tractability in inference relations. J. ACM 40: pp. 284-303 CrossRef
  64. McMillan, KL (2003) Interpolation and SAT-based model checking. In: Proceedings of the 15th Conference on Computer Aided Verification (CAV), volume 2725 of Lecture Notes in Computer Science. Springer, Berlin
  65. McMillan, KL (2005) An interpolating theorem prover. Theor. Comput. Sci. 345: pp. 101-121 CrossRef
  66. McMillan, KL Lazy abstraction with interpolants. In: ditors">Ball, T, Jones, R B eds. (2006) Proceedings of the 18th Conference on Computer Aided Verification (CAV), volume 4144 of Lecture Notes in Computer Science. Springer, Berlin, pp. 123-136
  67. McMillan, KL Quantified invariant generation using an interpolating saturation prover.. In: ditors">Ramakrishnan, C R, Rehof, J eds. (2008) Proceedings of the 14th Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science. Springer, Berlin, pp. 413-427
  68. McMillan, KL (2010) Lazy annotation for program testing and verification. In: Proceedings of the 22nd Conference on Computer Aided Verification (CAV), volume 6174 of Lecture Notes in Computer Science. Springer, Berlin
  69. McMillan, KL Interpolants from Z3 proofs. In: ditors">Bjesse, P, Slobodova, A eds. (2011) Proceedings of the 11th conference on formal methods in computer aided design (FMCAD). ACM and IEEE, New York
  70. Moska艂, M.: Fx7 or in software, it is all about quantifiers. System Descriptions at the Satisfiability Modulo Theories Competition (SMT-COMP) (2007). Available at http://research.microsoft.com/en-us/um/people/moskal/
  71. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Blaauw, D., Lavagno, L. (eds.) Proceedings of the 39th Design Automation Conference (DAC), pp. 530鈥?35 (2001)
  72. Mundici, D (1982) Complexity of Craig鈥檚 interpolation. Fundamenta Informaticae 5: pp. 261-278
  73. Nelson, G.: Techniques for Program Verification. PhD thesis, Stanford University, 1979. A revised version was published as Xerox PARC Computer Science Laboratory Research Report No. CSL-81-10
  74. Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W. W., Loveland, D. W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201鈥?11. American Mathematical Society (1983)
  75. Nelson, G, Oppen, DC (1979) Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1: pp. 245-257 CrossRef
  76. Nieuwenhuis, R, Oliveras, A, Tinelli, C (2006) Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53: pp. 937-977 CrossRef
  77. Pudl脿k, P (1997) Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic 62: pp. 981-998 CrossRef
  78. Rollini, SF, Sery, O, Sharygina, N Leveraging interpolant strength in model checking. In: ditors">Parthasarathy, M, Seshia, S A eds. (2012) Proceedings of the 24th Conference on Computer Aided Verification (CAV), volume 7358 of Lecture Notes in Computer Science. Springer, Berlin, pp. 193-209
  79. R眉mmer, P, Hojjat, H, Kuncak, V Disjunctive interpolation for Horn clause verification. In: ditors">Sharygina, N, Veith, H eds. (2013) Proceedings of the 25th Conference on Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science. Springer, Berlin, pp. 347-363
  80. R眉mmer, P., Suboti膰, P.: Exploring interpolants. In: Jobstmann, B., Ray, S. (eds.) Proceedings of the 13th Conference on Formal Methods in Computer Aided Design (FMCAD). FMCAD Inc (2013)
  81. Shankar, N (2009) Automated deduction for verification. ACM Comput. Surv. 41: pp. 40-96 CrossRef
  82. Smullyan, R.M.: First-order logic. Dover Publications, New York (1995). First published by Springer in 1968
  83. Sofronie-Stokkermans, V (2008) Interpolation in local theory extensions. Logical Methods in Computer Science 4: pp. Article 1 CrossRef
  84. Takeuti, G (1975) Proof theory, volume 81 of studies in logic. North Holland, Amsterdam
  85. Urquhart, A (1995) The complexity of propositional proofs. Bull. Symb. Log. 1: pp. 425-467 CrossRef
  86. Weissenbacher, G.: Program Analysis with Interpolants. PhD thesis, Magdalen College, Oxford University (2010)
  87. Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. Technical Report MSR-TR-2004-108, Microsoft Research (2004)
  88. Yorsh, G, Musuvathi, M A combination method for generating interpolants. In: ditors">Nieuwenhuis, R eds. (2005) Proceedings of the 20th Conference on Automated Deduction (CADE), volume 3632 of Lecture Notes in Artificial Intelligence. Springer, Berlin, pp. 353-368
  89. Zhang, L, Malik, S (2003) Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of the Conference on Design Automation and Test in Europe (DATE). IEEE, Los Alamitos
  
• 刊物类别：Computer Science
• 刊物主题：Mathematical Logic and Formal Languages
  Artificial Intelligence and Robotics
  Mathematical Logic and Foundations
  Symbolic and Algebraic Manipulation
  
• 出版者：Springer Netherlands
• ISSN：1573-0670

文摘

Interpolation is a deductive technique applied in program analysis and verification: for example, it is used to compute over-approximations of images or refine abstractions. An interpolation system takes a refutation and extracts an interpolant by building it inductively from partial interpolants. We survey color-based interpolation systems for ground proofs produced by key inference engines of state-of-the-art solvers: DPLL for propositional logic, equality sharing for combination of convex theories, and DPLL( \(\mathcal {T}\) ) for SMT-solving. Since color-based interpolation systems use colors to track symbols in proofs, equality is problematic, because replacement of equals by equals mixes symbols and therefore colors. We analyze interpolation in the presence of equality, and we demonstrate the color-based approach by giving a complete interpolation system for ground proofs by superposition.