Системы переписывания формул и их применение в автоматической верификации программ
Диссертация
Техника сужения представляет собой объединение переписывания и унификации. Эта техника проверки выполнимости формул исторически возникла как средство решения проблемы унификации в эквациональных теориях (Е'-унификации), была распространена на условные равенства и нашла применение как механизм, позволяющий объединять логические и функциональные языки. Разрешающие процедуры, основанные на сужении… Читать ещё >
Список литературы
- Абрамов С. А. Элементы анализа программ. — М.: Наука, 1986. — 128 с.
- Агафонов В.Н. Типы и абстракция данных в языках прокламирования (обзор) // Д""-:пые в языках программирования. -М.: Мир, 1982. — С. 265—327.
- Агафонов В.Н. Спецификация программ: понятийные средства и их организация. — Новосибирск: Наука, 1987. — 240 с.
- Алагич С., Арбиб М. Построение корректных структурированных программ. — М.: Радио и связь, 1984. — 264 с.
- Ануреев И. С. Интегрированные правила переписывания термов и их применение в автоматической верификации программ // Проблемы спецификации и верификации параллельных систем. — Новосибирск, 1995. — С. 185—213.
- Ануреев И. С. Системы переписывания формул. — Новосибирск, 1997. — 22 с. — (Препр./РАН. Сиб. отд-ние. ИСИ- № 40).
- Ануреев И.С. Упрощающие процедуры для типов данных, основанные на системах переписывания формул. — Новосибирск, 1998. — 43 с. — (Препр./РАН. Сиб. отд-ние. ИСИ- № 53).
- Ануреев И.С. Теория систем переписывания формул. — Новосибирск, 1998. — 35 с. — (Препр./РАН. Сиб. отд-ние. ИСИ: № 54).
- Ануреев И.С. Применение систем переписывания формул в автоматической верификации программ. — Новосибирск, 1998. — 47 с. — (Препр./РАН. Сиб. отд-ние. ИСИ- № 55).
- Ануреев И. С. Системы переписывания формул и их применение в автоматической верификации программ. — ИНПРИМ. Тезисы докладов, часть V. — Новосибирск: Изд-во Института математики СО РАН, 1998. — С. 37.
- Бухбергер Б., Лоос Р. Упрощение алгебраических выражений // Компьютерная алгебра. Символьные и алгебраические вычисления. — М.: Мир. 1986. — С. 23—65.
- Вирт Н. Алгоримы и структуры данных. — М.: Мир, 1989. — 360 с.
- Воробьев С.Г. Переписывающие методы доказательства теорем в импликативных над базисными теориях // Всесоюз. конф. по прикладной логике: Тез. докл. — Новосибирск: Ин-т математики СО РАН СССР, 1985. — С. 39—42.
- Воробьев С.Г. О выразительной силе систем переписывания термов // Применение методов математической логики (Секция «Представление знаний и синтез программ»): Тез. докл. IV Всесоюз. конф. — Таллин: Ин-т кибернетики АН ЭССР. 1986. — С. 48—50.
- Воробьев С.Г. О применении условных систем подстановок термов в верификации программ // Программирование. 1986. — № 4. — С. 3—14.
- Воробьев С.Г. О встраивании разрешимых фрагментов арифметики в системы переписывания термов // Методы трансляции и конструирования программ. — Новосибирск: ВЦ СО АН СССР, 1986.
- Воробьев С.Г. Системы условных редукций и их применение в проблемно-ориентированной верификации программ: Дис. канд. физ.-мат.наук:05.13.11. — Новосибирск, 1987. — 150 с.
- Воронков A.A., Дегтярев А. И. Автоматическое доказательство теорем I // Кибернетика. — 1986. — № 3. — С. 27—33.
- Вульф В., Лондон Р., Шоу М. Введение в построение и верификацию программ на языке Альфард // Данные в языках программирования. — М.: Мир, 1982. — С. 123—153.
- Глушков В.М., Капитонова Ю. В., Летичевский A.A. Инструментальные средства проектирования программ обработки математических текстов // Кибернетика. — 1979. — № 2. -С. 37—42.
- Грис Д. Наука программирования. — М.: Мир, 1984. — 416 с.
- Дейкстра Э. Дисциплина программирования. — М.: Мир, 1978. — 275 с.
- Замулин A.B. Типы данных в языках программирования и базах данных. — Новосибирск: Наука, 1987. — 150 с.
- Компьютерная алгебра. Символьные и алгебраические вычисления — М.: Мир, 1986. — 392 с.
- Кучеров Г. А. Системы подстановок термов. — Новосибирск. 1985. — 46 с. — (Препр./СО АН СССР. ВЦ- № 601).
- Маслов С.Ю., Минц Т. Е. Теория поиска вывода и обратный метод // Математическая логика и автоматическое доказательство теорем. — М.: Наука, 1983. — С. 291—314.
- Маслов С.Ю. О стратегиях метода резолюций и клаш-метода // Математическая логика и автоматическое доказательство теорем. — М.: Наука, 1983. — С. 326—332.
- Массер Д. Спецификация абстрактных типов данных в системе AFFIRM // Требования и спецификации в разработке программ. — М.: Мир, 1984. — С. 199—222.
- Мендельсон Э. Введение в математическую логику. — М.: Наука, 1976. — 320 с.
- Непомнящий В.А. ВеригЬикация программ над массивами // Системная информатика. Вып.З. Программные и вычислительные системы: Методы и языки анализа. — Новосибирск: ВО Наука. Сибирская издательская фирма, 1993. — С. 68—98.
- Непомнящий В.А., Рякин О. М. Прикладные методы верификации программ. — М.: Радио и связь, 1988. — 256 с.
- Непомнящий В. А. Сулимов А. А. Верификация программ линейной алгебры в системе СПЕКТР // Кибернетика и системный анализ. — 1992. — № 5. — С. 136—144.
- Непомнящий В. А. Сулимов А. А. Проблемно-ориентированные базы знаний и их применение в системе верификации программ СПЕКТР // Изв. РАН. Сер. Теория и системы управления. -1997. — № 2. — С. 169—175.
- Рабин М.О. Разрешимые теории // Справочная книга по математической логике. — М.: Наука, 1982. — Т. 3. — С. 77—111.
- Семенов A.JI. Разрешающие алгоритмы для логических теорий // Кибернетика и вычислительная техника. — М.: Наука, 1986. — Т. 2. — С. 134—146.
- Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. — М.: Наука, 1983. — 360 с.
- Ющенко Е.Л., Касаткина И. В. Современные методы доказательства правильности iiporpaMM // Кибернетика, 1980. — № 6. — С. 37—62.
- Apt K.R. Logic programming. Formal Models and Semantics // Handbook of Theor. Comput. Sci. — 1990. — Vol. B. — P. 495 574.
- Apt K.R. Ten years of Hoare’s logic: a survey. Part I // ACM Trans. Progr. Lang. Syst. — 1981. — Vol. 3, — № 4. — P. 431— 483.
- Bachmair L., Dershowitz N. Completion for rewriting modulo a congruence // Theor. Comput. Sci. —1989. — № 67 (2−3). — P. 173—202.
- Bachmair L., Dershowitz N. Commutation, transformation and termination // Lect. Notes Comput. Sci. — 1986. — Vol. 230.1. P. 5—20.
- Bachmair L., Ganzinger H. Rewrite-based equational theorem proving with selection and simplification // J. of Logic and Computation. — 1994. — № 4(3). — P. 1—31.
- Bachmair L., Plaisted D.A. Associative path ordering // Lect. Notes Comput. Sci. — 1985. — Vol. 202. — P. 241—254.
- Beckert B., Hahnle R., Oel P., Sulzmann M. The tableau-based theorem prover 3TAP, version 4.0 // Lect. Notes Comput. Sci. 1996. — Vol. 1104. — P. 303—307.
- Bergstra J.A., Klop J.W. Conditional rewrite rules: confluence and termination // J. Comput. and Syst. Sci. — 1986. — № 32 (3).1. P. 323—363.
- Buchberger B. Basic features and development of the Critical-pair/Completion procedure // Lect. Notes Comput. Sci. — 1985. — Vol. 202. — P. 1—45.
- Burstall R.M., Goguen J.A. The semantics of CLEAR, a specification language // Lect. Notes Comput. Sci. — 1980. — Vol. 86.1. P. 292—332.
- Clarke E.M. Programming language constructs for which it is possible to obtain good Hoare axiom system //J. ACM. — 1979. — Vol. 26, № 1. — P. 129—147.
- Comon H. Constraints in term algebras. An overview of constraint solving techniques // Lect. Notes Comput. Sci. — 1995. — Vol. 910. — P. 62—67.
- Dauchet M. Simulation of Turing machines by a left-linear rewrite rule // Lect. Notes Comput. Sci. — 1989. — Vol. 355. — P. 109— 120.
- De Champeaux D. About the Paterson-wegman linear unification algorithm //J. Comput. Syst. Sci. — 1986. — Vol. 32. — P. 79— 90.
- Comon H. Constraints in term algebras. An overview of constraint solving techniques // Lect. Notes Comput. Sci. — 1995. — Vol. 910. — P. 62—67.
- Dershowitz N. Computing with rewrite systems // Information and Control. — 1985. — Vol. 65. — P. 122—157.
- Dershowitz N. Ordering for term-rewriting systems // Proc. of the 20th Annual Symposi. on Foundations of Computer Science. San Juan, 1979. — P. 123—131.
- Dershowitz N. Termination // Lect. Notes Comput. Sci. — 1985.1. Vol. 202. — P. 180—224.
- Dershowitz N., Hoot C. Topics in termination // Lect. Notes Comput. Sci. — 1993. — Vol. 690. — P. 198—212.
- Dershowitz N., Jouannaud J.-P. Rewrite systems // Handbook of Theor. Comput. Sci. — 1990. — Vol. 6. — P. 243—320.
- Dershowitz N., Mitra S., Sivakumar G. Equation solving in conditional AC-theories // Lect. Notes Comput. Sci. — 1990. — Vol. 463. — P. 283—297.
- Dershowitz N., Sivakumar G. Solving goals in equational languages. // Lect. Notes Comput. Sci. — 1987. — Vol. 308. — P. 45—55.
- Dershowitz N., Plaisted D.A. Conditional rewriting // Software Eng.Notes. — 1985. — Vol. 10, № 4. — P. 55—59.
- Dershowitz N., Plaisted D.A. Logic programming cum applicative programming // Proc. of the 2nd IEEE Symposi. on Logic Programming. — Boston, 1985. — P. 54—66.
- Dershowitz N., Plaisted D.A. Equational programming // Machine Intelligence. — 1987. — № 11. — P. 21—56.
- Downey P.J., Sethi R., Tarjan R.E. Variations on the common subexpression problem //J. ACM. — 1980. — Vol. 27, № 4. — P. 758—771.
- Drosten K. Towards executable specification using conditional axioms // Lect. Notes Comput. Sci. — 1984. — Vol. 166. — P. 85 96.
- Echahed R. On completeness of narrowing strategies // Theor. Comput. Sci. — 1990. № 72. — P. 133—146.
- Echahed R. Uniform narrowing strategies // Lect. Notes. Comput. Sci. 1992. — № 632. — P. 259—275.
- Fay M. First-order unification in equational theories // Proc. of the 4th Internati. Workshop on Automated Deduction. — Austin. 1979. — P. 161—167.
- Ferro A., Omodeo E.G., Schwartz J.T. Decision Procedures for some fragments of set theory // Lect. Notes Comput. Sci. — 1980.1. Vol. 87. — P. 88—96.
- Fribourg L. A narrowing, procedure for theories with constructors // Lect. Notes Comput. Sci. — 1984. — Vol. 170. — P. 259—281.
- Fribourg L. SLOG: A logic programming language interpreter based on clausal superposition and rewriting // Proc. of the 2nd IEEE Symposi. on Logic Programming. — Boston, 1985. — P. 172—184.
- Ganzinger H., Giegerich R. A note on termination in combinations of heterogeneous term rewriting systems // Bull. Europ. Association for Theor. Comput. Sci. — 1987. — № 31. — P. 22—28.
- Gerhart S.L. An overview of AFFFIRM: a specification and verification system // Proc. IFIP Congress (Tokyo, Melbourne, 1980).
- Amsterdam: North-Holland, 1980. — P. 343—347.
- Gerhart S.L. Program verification in the 1980's // Proc. Conf. Computing in the 1980's. — Oregon, IEEE, 1978. — P. 80—98.
- Giovannetti E., Levi G., Moiso C., Palamidessi C. Kernel-LEAF: A logic plus functional language //J. Comput. and Syst. Sci. — 1991. — № 42. — P. 139—185.
- Goguen J.A., Meseguer J. EQLOG: Equality, types and generic modules for logic programming // Logic Programming: Functions. Relations and Equations. — Englewood cliffs: Prentice Hall. 1986.1. P. 295—363.
- Hanus M. Compiling logic programs with equality // Lect. Notes Comput. Sci. — 1990. — № 456. — P. 387—401.
- Holldobler S. Foundations of Equational Logic Programming // Lect. Notes Comput. Sci. — 1989. — Vol. 353. — P. 140—147.
- Hsiang J. Two results in term rewriting theorem proving // Lect. Notes Comput. Sci. — 1985. — Vol. 202. — P. 301—324.
- Hsiang J. Refutational theorem proving using term rewriting systems // Artif. Intell. — 1985. — Vol. 25, № 2. — P. 255—300.
- Hsiang J., Dershowitz N. Rewrite methods for clausal and non-clausal theorem proving / / Lect. Notes Comput. Sci. — 1983. — Vol. 154. — P. 331—346.
- Hsiang J., Kirchner H., Lescanne P., Rusinowitch M. Automated theorem proving in the presence of equalities // J. Automat. Re-seach. — 1992. — Vol. 14. — P.71—100.
- Huet G., Hullot J.M. Proofs by induction in equational theories with constructors //J. Comput. System Sci. — 1982. — Vol. 25, No 2. — P. 239—266.
- Huet G., lankford D.S. On the uniform halting problem for term rewriting systems. — Paris, 1978. — (INRIA Lab.- Rep. № 283).
- Huet G., Oppen D.C. Equation and rewrite rules. A survey // Formal language theory: Perspectives and Open Problems. — New York: Acad. Press, 1980. — P. 349—406.
- Huet G. Confluent reductions: abstract properties and applications to term rewriting systems //J. ACM. — 1980. — Vol. 27. № 4. — P. 797—821.
- Hullot J.M. Canonical forms and unification // Lect. Notes Comput. Sci. — Vol. 87. — 1980. — P. 318—334.
- Hufimann H. Unification in conditional-equational theories // Lect. Notes Comput. Sci. — Vol. 204. — 1985. — P. 543—553.
- Igarashi S., London R.L., Luckham D.C. Automatic program verification I: a logical basis and its implementation // Acta Informatica. — 1975. — Vol. 4, № 2. — P. 145—182.
- Jantzen M. Confluent string rewriting and congruences // Europ. Association for Theor. Comput. Sci., Monographs on Theor. Com-put. Sci. — 1988. — Vol. 14. — P. .
- Jouannaud J.P. Confluent and coherent equational term rewriting systems: applications to proofs in abstract data types // Lect. Notes Comput. Sci. — 1983. — Vol. 159. — P. 269—283.
- Jouannaud J.P., Kirchner H. Completion of a set of rules modulo a set of equations // SIAM J. of Computing. — 1986. — № 15 (4).1. P. 1155—1194.
- Jouannaud J.P., March e C. Copletion modulo associativity, com-mutativity and identity (ACI) // Lect. Notes Comput. Sci. — 1990.1. Vol. 429. — P. 111—120.
- Jouannaud J.P., Waldmann B. Reductive conditional term rewriting systems // Proc. of the 3rd IFIP Working Conference on Formal Description of Programming Concepts. — Ebberup, 1986. — P. 223—244.
- Kaplan S. Conditional rewrite rules // Theor. Comput. Sci. —1984. — Vol. 33, № 2−3. — P. 175—193.
- Kaplan S. Simplifying conditional term rewriting systems: unification, termination and confluence //J. Symb. Comput. — 1987.4(3). — P. 295—334.
- Kapur D., Narendran P. An equational approach to theorem proving in first order predicate calculus // Software Eng. Notes.1985. — Vol. 10, № 4. — P. 63—66.
- Kirchner H. On the use of constraints in automated deduction // Lect. Notes Comput. Sci. — 1995. — Vol. 910. — P. 128—146.
- Klop J.W. Term rewriting systems // Handbook Logic Comp. Sci.1993. — Vol. 2. — P. 1—116.
- Klop J.W. Combinatory reduction systems // Mathematical Centre Tracts. CWI, Amsterdam, 1980.
- Kruskal J.B. Well-quasi-ordering, the tree theorem and Vaz-sonyi's conjecture // Trans. AMS. — 1960. — № 95. — P. 210—225.
- Lankford D.S. Some approaches to equality for computational logic: a survey and assessment. — Univ. of Texas, 1977. — (Rep. ATP-36).
- Lescanne P. Term rewriting systems and algebra // Lect. Notes Comput. Sci. — 1984. — Vol. 170. — P. 166—174.
- Letz R., Schumann J. Bayerl S., Bidel W. SETHEO: A highperformance theorem prover //J. Automat. Reasoning. — 1992. — Vol. 8, № 2. — P. 183—212.
- Loweland D.W. Automated theorem proving: a quarter century review // Contemporary Mathematics. — 1984. — Vol. 29. — P. 1—42.
- Manna Z., Waldinger R. The logic of computer programming // IEEE Trans. Software Eng. — 1978. — Vol. SE-4, № 3. — P. 199— 229.
- Martelli A., Montanari U. An efficient unification algorithm // ACM Trans. Prog. Lang, and Syst. — 1982. — Vol. 4, № 2. — P. 258—282.
- Mateti P. A decision procedure for the correctness of a class of programs // J. ACM. — 1981. — Vol. 28, № 2. — P. 215—232.
- Meinke K., Tucker J.V. Universal algebra. // Handbook Logic Comp. Sci. — 1992. — Vol. 1. — P. .
- Middeldorp A. A sufficient condition for the termination of the direct sum of term rewriting systems // Proc. of. the 4th IEEE
- Symposi. on Logic in Comput. Sci. — Pacific Grove, 1989. — P. 396—401.
- Moreno-Navarro J.J., Rodriguez-Artalejo M. BABEL: A functional and logic programming language based on constructor discipline and narrowing // Lect. Notes Comput. Sci. — 1989. — Vol. 343. — P. 223—232.
- Moriconi M., Schwartz R.L. Automatic construction of verification condition generators from Hoare’s logics // Lect. Notes Comput. Sci. — 1981. — Vol. 115. — P. 363—377.
- Navarro M., Orejas F. On the equivalence of hierarchical and non-hierarchical rewriting in conditional term rewriting systems // Lect. Notes Comput. Sci. — 1984. — Vol. 174. — P. 74—85.
- Nederpelt R.P. Strong normalization for a typed lambda calculus with lambda structured types. PhD thesis, Technische HogeschooL Eindhoven, The Netherlands, 1973.
- Nelson G. Combining satisfiability procedures by equality sharing // Contemporary Mathematics. — 1984. — Vol. 29. — P. 201— 211.
- Nelson G., Oppen D.C. Simplification by cooperating decision procedures // ACM Trans. Progr. Lang. Syst. — 1979. — Vol. 1. № 2. — P. 245—257.
- Nelson G., Oppen D.C. Fast desition procedures based on congruence closure //J. ACM.. 1980. — Vol. 27, № 2. — P. 356—364.
- Nepomniaschy V.A. On a symbolic method of verification for definite iteration over data structures // Joint Bulletin of the Institute of Informatics Systems and Computer Center. — 1998. — № 5. — P. 1—22.
- Nepomniaschy V.A., Sulimov A.A. Problem-Oriented Means of Program Specification and Verification in Project SPECTRUM // Lect. Notes Comput. Sci. — 1993. — Vol. 722. — P. 374—378.
- Nepomniaschy V.A., Sulimov A.A. Towards Automatic Program Verification: Problem-Oriented Knowledge Bases // Specification, verification and net models of concurrent systems. — Novosibirsk, 1994. — P. 138—150
- Nutt W., Rety P., Smolka G. Basic narrowing revisited //J. Symb. Comput. — 1989. — № 7. — P. 295—317.
- Oppen D.C. Reasoning about recursively defined data structures // J. ACM. — 1980. — Vol. 27, № 3. — P. 403—411.
- Oppacher F., Suen E. HARP: A tableau-based theorem prover // J. Automat. Reasoning. — 1988. — Vol. 4. — P. 69—100.
- Owre S., Rushby J., Shankar N. PVS: A prototype verification system // Lect. Notes Art. Intell. — 1992. — Vol. 607. — P. 748 752.
- Oyamaguchi M. The Church-Rosser property for ground term rewriting systems is decidable // Theor. Comput. Sci. — 1987. — № 49 (1). — P. 43−79.
- Paul E. Equational methods in first order predicate calculus // J. Symb. Comput. — 1985. — № 1. — P. 7—29.
- Peterson G.E., Stickel M.E. Complete sets of reductions for some equational theories //J. ACM. — 1981. — Vol. 28, No 2. P. 233—264.
- Plaisted D.A. A recursively defined ordering for proving termination of term rewriting systems. — University of Illinois, 1978. — (Dept. of Computer Science- Rep. UIUCDCS-R-78−943).
- Remy J.-L., Zhang H. REVEUR 4: A system for validating conditional algebraic specifications of abstract data types // Proc. 6th Europ. Conf. on Artificial Intell. (ECAI-84). —, 1984. — P.563−572.
- Rety P. Improving basic narrowing techniques // Lect. Notes Comput. Sci. — 1987. — Vol. 256. — P. 228—241.
- Rusinowitch M. On termination of the direct sum of term rewriting systems. // Information Processing Letters. — 1987. — № 26.1. P. 65—70.
- Rusinowitch M. Path of subterms ordering and recursive decomposition ordering revisited // J. of Symb. Comput. — 1987. — .№ 3.1. P. 117—131.
- Schwartz J.T. A survey of program proof technology. — New York Univ., 1978. — (Dep. Comput. Sci.- Rep. № 001).
- Shostak R.E. On the SUP-INF method for proving Presburger formulas // J. ACM. — 1977. — Vol. 24, № 4. — P. 529—543.
- Shostak R.E. A practical decision procedure for arithmetic with function symbols // J. ACM. — 1979. — Vol. 26, № 2. — P. 351— 360.
- Shostak R.E. Deciding linear inequalitities by computing loop residues // J. ACM. — 1981. — Vol. 28, № 4. — P. 769—779.
- Shostak R.E., Schwartz R., Melliar-Smith P.M. STP: A mechanized logic for specification and verification // Lect. Notes Corn-put. Sci. — 1984. — Vol. 170. — P. 1—42.
- Siekmann J. Universal unification // Lect. Notes Comput. Sci. — 1984. — Vol. 170. — P. 1—42.
- Staples J. Church-Rosser theorems for replacement systems // Algebra and Logic, Lect. Notes in Math. — 1975. — Vol. 450. — R 291—307.
- Steinbach J. Simplification ordering: history of results // Fundamenta Informaticae. — 1995. — Vol. 24, № 1. — P.47—87.
- Suzuki N., Jefferson D. Verification decidability of Presburger array programs // J. ACM. — 1980. — Vol. 27, № 1. — P. 191— 205.
- Toyama Y. On the Church-Rosser property for the direct sum of term rewriting systems //J. ACM. — 1987. — № 34 (1). — P. 128—143.
- Toyama Y., Klop J.W., Barendregt H.P. Termination for the direct sum of left-linear term rewriting systems // Lect. Notes Com-put. Sci. — 1989. — Vol. 355. — P. 477—491.
- Yamamoto A. Completeness of extended unification based on basic narrowing // Proc. of the 7th Logic Programming Conference.
- Jerusalem, 1988. — P. 1—10.
- You Y.H. Enumerating outer narrowing derivations for constructor based term rewritm0* ystems //J. Symb. Comput. — 1989.7. — P. 319—343.
- Zhang H., Kapur D. Unnecessary inferences in associative-commutative completion procedures // Mathe. Systems Theory.1990. — № 23. — P. 175—206.
- Zhang H., Remy J.-L. Contextual rewriting // Lect. Notes Comput. Sci. — Vol. 202. — P. 46—62.