×

Automatic decidability and combinability. (English) Zbl 1216.68163

Summary: Verification problems can often be encoded as first-order validity or satisfiability problems. The availability of efficient automated theorem provers is a crucial pre-requisite for automating various verification tasks as well as their cooperation with specialized decision procedures for selected theories, such as Presburger Arithmetic. In this paper, we investigate how automated provers based on a form of equational reasoning, called paramodulation, can be used in verification tools. More precisely, given a theory \(T\) axiomatizing some data structure, we devise a procedure to answer the following questions. Is the satisfiability problem of \(T\) decidable by paramodulation? Can a procedure based on paramodulation for \(T\) be efficiently combined with other specialized procedures by using the Nelson-Oppen schema? Finally, if paramodulation decides the satisfiability problem of two theories, does it decide satisfiability in their union?
The procedure capable of answering all questions above is based on schematic saturation; an inference system capable of over-approximating the inferences of paramodulation when solving satisfiability problems in a given theory \(T\). Clause schemas derived by schematic saturation describe all clauses derived by paramodulation so that the answers to the questions above are obtained by checking that only finitely many different clause schemas are derived or that certain clause schemas are not derived.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B70 Logic in computer science
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Armando, A.; Bonacina, M. P.; Ranise, S.; Schulz, S., On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal, (Gramlich, B., Proc. of the 5th Int. Workshop on Frontiers of Combining Systems (FroCoSʼ2005). Proc. of the 5th Int. Workshop on Frontiers of Combining Systems (FroCoSʼ2005), Lecture Notes in Computer Science, vol. 3717 (September 2005), Springer: Springer Vienna, Austria), 65-80 · Zbl 1171.68507
[2] Armando, A.; Ranise, S.; Rusinowitch, M., A rewriting approach to satisfiability procedures, J. Inform. Comput., 183, 2, 140-164 (June 2003)
[3] T. Ball, S.K. Rajamani, The SLAM project: Debugging system software via static analysis, in: Principle of Programming Languages (POPLʼ02), 2002, pp. 1-3.; T. Ball, S.K. Rajamani, The SLAM project: Debugging system software via static analysis, in: Principle of Programming Languages (POPLʼ02), 2002, pp. 1-3.
[4] Basin, D. A.; Ganzinger, H., Automated complexity analysis based on ordered resolution, J. ACM, 48, 1, 70-109 (2001) · Zbl 1320.68163
[5] Bonacina, M. P.; Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D., Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures, (Proc. of the 3rd Int. Conference on Automated Reasoning (IJCARʼ06). Proc. of the 3rd Int. Conference on Automated Reasoning (IJCARʼ06), Seattle, WA, USA. Proc. of the 3rd Int. Conference on Automated Reasoning (IJCARʼ06). Proc. of the 3rd Int. Conference on Automated Reasoning (IJCARʼ06), Seattle, WA, USA, Lecture Notes in Artificial Intelligence, vol. 4130 (August 2006), Springer), 513-527 · Zbl 1222.03011
[6] Bouillaguet, C.; Kuncak, V.; Wies, T.; Zee, K.; Rinard, M., Using first-order theorem provers in the Jahob data structure verification system, (Verification, Model Checking and Abstract Interpretation (VMCAIʼ07). Verification, Model Checking and Abstract Interpretation (VMCAIʼ07), Lecture Notes in Computer Science, vol. 4349 (2007), Springer), 74-88 · Zbl 1132.68348
[7] Dershowitz, N.; Jouannaud, J.-P., Handbook of Theoretical Computer Science, vol. B, Rewrite Systems (1990), Elsevier and MIT Press, pp. 244-320 (Chapter 6)
[8] Detlefs, D.; Nelson, G.; Saxe, J. B., Simplify: a theorem prover for program checking, J. ACM, 52, 3, 365-473 (2005) · Zbl 1323.68462
[9] Filliâtre, J.-C.; Marché, C., The why/krakatoa/caduceus platform for deductive program verification, (Computer Aided Verification, 19th International Conference, Proceedings. Computer Aided Verification, 19th International Conference, Proceedings, CAV 2007, Berlin, Germany. Computer Aided Verification, 19th International Conference, Proceedings. Computer Aided Verification, 19th International Conference, Proceedings, CAV 2007, Berlin, Germany, Lecture Notes in Computer Science, vol. 4590 (2007), Springer), 173-177
[10] Ganzinger, H.; McAllester, D. A., Logical algorithms, (18th International Conference on Logic Programming (ICLPʼ02). 18th International Conference on Logic Programming (ICLPʼ02), Lecture Notes in Computer Science, vol. 2401 (2002), Springer), 209-223 · Zbl 1045.68061
[11] Ganzinger, H.; Waldmann, U., Theorem proving in cancellative abelian monoids, (McRobbie, M. A.; Slaney, J. K., Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, Proceedings. Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, Proceedings, New Brunswick, NJ, USA, 1996. Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, Proceedings. Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, Proceedings, New Brunswick, NJ, USA, 1996, Lecture Notes in Computer Science, vol. 1104 (1996), Springer), 388-402 · Zbl 1412.68225
[12] Ge, Y.; Barrett, C.; Tinelli, C., Solving quantified verification conditions using satisfiability modulo theories, (Proc. of the 21st Int. Conference on Automated Deduction (CADEʼ07). Proc. of the 21st Int. Conference on Automated Deduction (CADEʼ07), Lecture Notes in Artificial Intelligence, vol. 4603 (July 2007), Springer: Springer Bremen, Germany), 167-182 · Zbl 1213.68376
[13] Givan, R.; McAllester, D. A., Polynomial-time computation via local inference relations, ACM Trans. Comput. Log., 3, 4, 521-541 (2002) · Zbl 1365.68202
[14] Godoy, G.; Nieuwenhuis, R., Superposition with completely built-in abelian groups, J. Symbolic Comput., 37, 1, 1-33 (2004) · Zbl 1043.03011
[15] Kirchner, H.; Ranise, S.; Ringeissen, C.; Tran, D.-K., On superposition-based satisfiability procedures and their combination, (Proc. of Second International Colloquium on Theoretical Aspects of Computing (ICTACʼ05). Proc. of Second International Colloquium on Theoretical Aspects of Computing (ICTACʼ05), Hanoi, Vietnam. Proc. of Second International Colloquium on Theoretical Aspects of Computing (ICTACʼ05). Proc. of Second International Colloquium on Theoretical Aspects of Computing (ICTACʼ05), Hanoi, Vietnam, Lecture Notes in Computer Science, vol. 3722 (Oct. 2005), Springer), 594-608 · Zbl 1169.68509
[16] Kirchner, H.; Ranise, S.; Ringeissen, C.; Tran, D.-K., Automatic combinability of rewriting-based satisfiability procedures, (Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPARʼ06). Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPARʼ06), Lecture Notes in Artificial Intelligence, vol. 4246 (November 2006), Springer: Springer Phnom Penh, Cambodia), 542-556, (subseries of Lecture Notes in Computer Science) · Zbl 1165.68490
[17] Lewis, H. R., Renaming a set of clauses as a horn set, J. ACM, 25, 134-135 (1978) · Zbl 0365.68082
[18] Lynch, C.; Morawska, B., Automatic decidability, (Proc. of 17th IEEE Symposium on Logic in Computer Science (LICSʼ02). Proc. of 17th IEEE Symposium on Logic in Computer Science (LICSʼ02), Copenhagen, Denmark, July 22-25 (2002), IEEE Computer Society Press), 7-16
[19] Lynch, C.; Tran, D.-K., Automatic decidability and combinability revisited, (Proc. of the 21st Int. Conference on Automated Deduction (CADEʼ07). Proc. of the 21st Int. Conference on Automated Deduction (CADEʼ07), Lecture Notes in Artificial Intelligence, vol. 4603 (July 2007), Springer: Springer Bremen, Germany), 328-344 · Zbl 1213.68573
[20] McAllester, D. A., Automatic recognition of tractability in inference relations, J. ACM, 40, 2, 284-303 (1993) · Zbl 0770.68106
[21] G. Nelson, Techniques for program verification, Technical Report CS-81-10, Xerox Palo Research Center California, USA, 1981.; G. Nelson, Techniques for program verification, Technical Report CS-81-10, Xerox Palo Research Center California, USA, 1981.
[22] Nelson, G.; Oppen, D. C., Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst., 1, 2, 245-257 (Oct. 1979)
[23] Nieuwenhuis, R.; Rubio, A., Paramodulation-based theorem proving, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning (2001), Elsevier and MIT Press), 371-443 · Zbl 0997.03012
[24] Oppen, D. C., Reasoning about recursively defined data structures, J. ACM, 27, 3, 403-411 (1980) · Zbl 0477.68025
[25] Ranise, S.; Ringeissen, C.; Tran, D.-K., Nelson-Oppen, Shostak and the extended canonizer: A family picture with a newborn, (Proc. of First International Colloquium on Theoretical Aspects of Computing (ICTACʼ04). Proc. of First International Colloquium on Theoretical Aspects of Computing (ICTACʼ04), Guiyang, China. Proc. of First International Colloquium on Theoretical Aspects of Computing (ICTACʼ04). Proc. of First International Colloquium on Theoretical Aspects of Computing (ICTACʼ04), Guiyang, China, Lecture Notes in Computer Science, vol. 3407 (Sep. 2004), Springer), 372-386 · Zbl 1108.68574
[26] Ranise, S.; Ringeissen, C.; Zarba, C. G., Combining data structures with nonstably infinite theories using many-sorted logic, (Gramlich, B., Proc. of the 5th Int. Workshop on Frontiers of Combining Systems (FroCoSʼ05). Proc. of the 5th Int. Workshop on Frontiers of Combining Systems (FroCoSʼ05), Lecture Notes in Computer Science, vol. 3717 (September 2005), Springer: Springer Vienna, Austria), 48-64 · Zbl 1171.68439
[27] A. Riazanov, A. Voronkov, Splitting without backtracking, in: Proc. of 7th International Joint Conference on Artificial Intelligence (IJCAIʼ01), Seattle, Washington, USA, August 4-10, 2001, pp. 611-617.; A. Riazanov, A. Voronkov, Splitting without backtracking, in: Proc. of 7th International Joint Conference on Artificial Intelligence (IJCAIʼ01), Seattle, Washington, USA, August 4-10, 2001, pp. 611-617.
[28] Schumann, J. M., Automated Theorem Proving in Software Engineering (2001), Springer
[29] Stuber, J., Superposition theorem proving for abelian groups represented as integer modules, Theoret. Comput. Sci., 208, 1-2, 149-177 (1998) · Zbl 0912.68187
[30] Tinelli, C.; Harandi, M. T., A new correctness proof of the Nelson-Oppen combination procedure, (Baader, F.; Schulz, K. U., Frontiers of Combining Systems: Proceedings of the 1st International Workshop (FroCosʼ96). Frontiers of Combining Systems: Proceedings of the 1st International Workshop (FroCosʼ96), Munich, Germany. Frontiers of Combining Systems: Proceedings of the 1st International Workshop (FroCosʼ96). Frontiers of Combining Systems: Proceedings of the 1st International Workshop (FroCosʼ96), Munich, Germany, Applied Logic (Mar. 1996), Kluwer Academic Publishers), 103-120 · Zbl 0893.03001
[31] Tinelli, C.; Zarba, C. G., Combining nonstably infinite theories, J. Automat. Reason., 34, 3, 209-238 (Apr. 2005)
[32] D.-K. Tran, Conception de Procédure de Décision par Combinaison et Saturation, PhD thesis, LORIA - Université Henri Poincaré, Nancy, France, 2007.; D.-K. Tran, Conception de Procédure de Décision par Combinaison et Saturation, PhD thesis, LORIA - Université Henri Poincaré, Nancy, France, 2007.
[33] van Dalen, D., Logic and Structure (1989), Springer · Zbl 0714.03001
[34] Waldmann, U., Superposition for divisible torsion-free abelian groups, (Kirchner, C.; Kirchner, H., Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Proceedings. Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Proceedings, Lindau, Germany, 1998. Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Proceedings. Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Proceedings, Lindau, Germany, 1998, Lecture Notes in Computer Science, vol. 1421 (1998), Springer), 144-159 · Zbl 0924.03026
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.