Verification of programs: status, problems and experimental results. I
Abstract
Full Text:
PDF (Русский)References
Kaufmann M., Manolios P., Moore J.S. Computer Aidede Reasoning: An Approach // Kluwer Academic Publishers. – 2000. – 212 p.
Nipkow T., Paulson L., Wenzel M. Isabelle/HOL: A Proof Assistant for Higher Order Logic, // Springer Verlag. – 2002. – LNCS. – Vol. 2283. – P. 3–51.
Oppen D.C., Cook S.A. Proving Assertion About Programs that Manipulate Data Structures // In Proceed. Of the 7-th Annual ACM
Symposium on Theory of Computing (STOC 1975). – Aluquerque. – NM. – ACM Press. – 1975. – P. 107–116.
Clarke E.M., Emerson E.A. Design and Synthesis of Synchronization Skeleton Using Branching Time Temporal Logic. In D.C. Kozen, edit // Logic of Program Workshop. – Springer Verlag. – 1981. – LNCS. – Vol. 131. – P. 52–71.
Queille J.P., Sifakis J. Proving Specification and Verification of Concurent Systems in CESAR // In Proceed. of the 5–th Intern.
Symposium on Programming. – Springer Verlag. – 1982. – LNCS. – Vol. 137. – P. 373–351.
Jones R. B. Simbolic Simulation Method for Industrial Formal Verification // Kluwer Academic Publishers. – 2002. – 286 p.
Chou C. The Mathematical Foundation of Symbolic Trajectory Evaluation. In N. Halbwacha and D. Peled, edit // Proc. of the
–th International Conference on Computer Aided Verification (CAV 1999). – SpringerVerlag.– 1999. – LNCS. – Vol. 1633. – P. 196–207.
Ray. S. Scalable Techniques for Formal Verificaton // Springer Science+Business Media. – 2010. – LLC. – P. 9–57.
Vardi M.Y., Wolper P. An Automata–theoretic Approach to Linear Temporal Logic // Logics for Concurrency: Structure versus
Automata Springer Verlag. – 1966. – LNCS. – Vol. 1043. – P. 238–266.
Кларк E.M., Грамберг O., Пелед Д. Верификация моделей программ: Model Chcking. – M.: МЦНМО, 2000. – 416 c.
Карпов Ю.Г. MODEL CHECKING. Верификация паралелельных и распределенных программных систем. – Санкт–Петербург: БХВ–Петербург, 2010. – 560 с.
Jensen K., Kristensen L.M. Colored Petri Nets: Modelling and Validation of Concurent Systsems. Springer Verlag. – 2009. – P. 384.
Penczek W., Polrola A. Advanced in Verification of Time Petri Nets and Timed Automata. Springer Verlag. – 2006. – P. 256.
Hoare C.A.R. An axiomatic basis of computer programming // CACM. –1969. – Vol. 12. – P. 576–580.
Cocke J., Schwartz J.T. Programming Language and their Compilers // Courant Institute of Mathem. Sciences. – New York University.
– 1970. – N.Y. – P. 3–21.
Аllen F.E. Interprocedural analysis // ACM SIGPLAN Notices. – 1976. – Vol. 6, N 7. – P. 23 – 31.
Летичевский А.А. Эквивалентность и оптимизация программ // Труды междунар. симпозиума по теоретическому программированию. – Новосибирск, 1972. – С. 166–180.
Kildall G.A. A unified approach to program optimization // Conf. Rec. of ACM Symp. on Prince. of Program Languages, Boston, Massachusetts, Oktober 1–3, 1973. – P. 194–206.
Kam J.B., Ullman D.J. Monotone data flow analysis frame works // Acta Inform. – 1978. – Vol. 3. – P. 305–318.
Касьянов В.Н. Учет априорной информации при анализе свойств состояний программ // Математическая теория программирования. – Новосибирск: ВЦ СО АН СССР, 1985. – С. 150–157.
Годлевский А.Б., Капитонова Ю.В., Кривой С.Л. и др. Итеративные методы анализа программ. Равенства и неравенства //
Кибернетика. – 1990. – № 3. – С. 1–9.
Кривой С.Л. О поиске инвариантных соотношений в программах. // Математическая теория проектирования вычислительных машин. – Киев: ИК АН УССР. – 1978. – С. 35–51.
Сабельфельд В.К. Учет свойств операций при глобальном анализе свойств программ // Математическая теория программирования. – Новосибирск: ВЦ СО АН СССР. – 1985. – С. 132–149.
Иткин В.Э. Логико–термальная эквивалентность схем программ // Кибернетика. – 1972. – № 1. – C. 5–27.
Cousot P., Halbwochs N. Discovery of Linear Restraints Among Variables of Program // Conf. Record of the 5–th Annual ACM Symposium on Princieples of Programming Languages. – USA. – 1978. – P. 84–96.
Cousot P. Abstract Interpretation Based Formal Methods and Future Challenges // Informatics LNCS. – Vol. 2000, 2001. – P. 138–156.
Muller–Olm M., Seidl H. Computing Interprocedurally Valid Relations in Affine Programs. // Symposium on Principles of Programming Languages, 2004.
Костырко В.С., Бакулин А.В. Об индуктивном синтезе инвариантных утверждений и функций программ // Кибернетика. –
– № 1. – C. 18–24.
Karr M. Affine Relationships Among Variables of a Program // Acta Informatica. – 1976. – № 6. – P. 133–151.
Годлевский А.Б., Кривой С.Л. Применение техники смешанных вычислений к построению эффективных алгоритмов унификации и приведения выражений // Тезисы докл. Всесоюз. конф. "Методы трансляции и конструирования программ". – Новосибирск, 1988. – С. 59–62.
Абрамов С.А. Элементы анализа программ. – М.: Наука, 1988. – С. 129.
Дейкстра Э. Дисциплина программирования. – М.: Мир, 1975. – С. 247.
Летичевский А.А. Об одном подходе к анализу программ // Кибернетика. – 1979. – № 6. – C. 1–8.
Refbacks
- There are currently no refbacks.