Extending \(H_1\)-clauses with disequalities. (English) Zbl 1260.68115
Summary: The class \(H_{1}\) has proven particularly useful for the analysis of term-manipulating programs such as cryptographic protocols. Here, we show that clauses from that class can be extended with disequalities between arbitrary terms while retaining decidability of satisfiability. The proof is based on a normalization procedure together with a procedure to decide whether a finite automaton with disequalities accepts less than \(k\) elements, and a subtle combinatorial argument to prove that only finitely many disequalities need to be considered.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q45 | Formal languages and automata |
Keywords:
formal methods; program analysis; Horn clauses; term disequalities; \(H_{1}\)-normalization; finite tree automataReferences:
| [1] | Blanchet, Bruno, An efficient cryptographic protocol verifier based on Prolog rules, (14th IEEE Computer Security Foundations Workshop (CSFW-14). 14th IEEE Computer Security Foundations Workshop (CSFW-14), Cape Breton, Nova Scotia, Canada (June 2001), IEEE Computer Society), 82-96 |
| [2] | Thom W. Frühwirth, Ehud Y. Shapiro, Moshe Y. Vardi, Eyal Yardeni, Logic programs as types for logic programs, in: Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS), 15-18 July, 1991, Amsterdam, The Netherlands, 1991, pp. 300-309.; Thom W. Frühwirth, Ehud Y. Shapiro, Moshe Y. Vardi, Eyal Yardeni, Logic programs as types for logic programs, in: Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS), 15-18 July, 1991, Amsterdam, The Netherlands, 1991, pp. 300-309. |
| [3] | Goubault-Larrecq, Jean, Deciding H1 by resolution, Information Processing Letters, 95, 3, 401-408 (August 2005) · Zbl 1185.68620 |
| [4] | Goubault-Larrecq, Jean; Parrennes, Fabrice, Cryptographic protocol analysis on real C code, (Cousot, Radhia, Verification, Model Checking, and Abstract Interpretation. Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, vol. 3385 (2005), Springer: Springer Berlin/Heidelberg), 363-379 · Zbl 1111.68506 |
| [5] | Nevin Heintze, Set-based analysis of ML programs, in: Proceedings of the 1994 ACM Conference on LISP and Functional Programming, Orlando, Florida, USA, 1994, pp. 306-317.; Nevin Heintze, Set-based analysis of ML programs, in: Proceedings of the 1994 ACM Conference on LISP and Functional Programming, Orlando, Florida, USA, 1994, pp. 306-317. |
| [6] | J. Mongy, Transformation de noyaux reconnaissables dʼarbres, PhD thesis, Laboratoire dʼInformatique Fondamentale de Lille, Université des Sciences et Technologies de Lille, Villeneuve dʼAscq, France, 1981.; J. Mongy, Transformation de noyaux reconnaissables dʼarbres, PhD thesis, Laboratoire dʼInformatique Fondamentale de Lille, Université des Sciences et Technologies de Lille, Villeneuve dʼAscq, France, 1981. |
| [7] | Müller-Olm, Markus; Rüthing, Oliver; Seidl, Helmut, Checking Herbrand equalities and beyond, (Cousot, Radhia, Verification, Model Checking, and Abstract Interpretation (VMCAIʼ2005). Verification, Model Checking, and Abstract Interpretation (VMCAIʼ2005), Lecture Notes in Computer Science, vol. 3385 (2005), Springer: Springer Berlin/Heidelberg), 79-96 · Zbl 1112.68094 |
| [8] | Nielson, Flemming; Riis Nielson, Hanne; Seidl, Helmut, Normalizable Horn clauses, strongly recognizable relations, and Spi, (Proceedings of the 9th International Symposium on Static Analysis. Proceedings of the 9th International Symposium on Static Analysis, Lecture Notes in Computer Science, vol. 2477 (2002), Springer-Verlag: Springer-Verlag London, UK), 20-35 · Zbl 1015.68042 |
| [9] | Reuß, Andreas; Seidl, Helmut, Bottom-up tree automata with term constraints, (Fermüller, Christian G.; Voronkov, Andrei, Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 17th International Conference, LPAR-17. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 17th International Conference, LPAR-17. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010, Lecture Notes in Computer Science, vol. 6397 (2010)), 581-593 · Zbl 1306.68096 |
| [10] | Weidenbach, Christoph, Towards an automatic analysis of security protocols in first-order logic, (Ganzinger, Harald, Proceedings of the 16th International Conference on Automated Deduction. Proceedings of the 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999. Proceedings of the 16th International Conference on Automated Deduction. Proceedings of the 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Lecture Notes in Computer Science, vol. 1632 (1999), Springer), 314-328 · Zbl 1038.94548 |
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.
