Логика ветвящегося времени как инструмент спецификации и верификации параллельных программ.
Article Sidebar
Опубликован:
04.11.1993
Main Article Content
Аннотация
В настоящей статье рассматриваются вопросы, связанные с использованием формализма логики ветвящегося времени для описания вычислительных свойств и верификации параллельных программ.
Скачивания
Данные скачивания пока не доступны.
Article Details
Как цитировать
Стеблецова В. Логика ветвящегося времени как инструмент спецификации и верификации параллельных программ. // Логические исследования / Logical Investigations. 1993. Т. 2. C. 159-169.
Выпуск
Раздел
Статьи
Литература
Ben-Ari М.у Manna Z., Pnueli A.. The temporal logic of branching time / / Acta Informatica. Vol.20. 1983. P.207-226.
Clarke E.f Emerson E. Using branching time logic to synthesize synchronization skeletons//Science of Computing Programming. Vol. 1982. P.241-266.
Emerson E.f Halpem J. "Sometimes" and "not never" revisited: on branching versus linear time//Proc. ACM Symposium on Principles of Programming Languages. Paris, 1983. P.127-140.
Floyd R. Assigning meaning to programs//Proc. of Symposium in Applied Mathematics. N.Y., 1967. P.19-32.
CabbayD., PhueliA., Shelah S., StaviJ. On temporal analysis of fairness //Proc. of ACM Symposium on Principles of Programming Languages. Las-Vegas, 1980. P.163-173.
Kroger F. A generalised nexttime operator in temporal logic / / J. of Computer and System Science. Vol.29. № 1.1984. P.80-98.
Lamport L. "Sometimes" is sometimes "not never" //Proc. of ACM Symposium on Principles of Programming Languages. Las-Vegas, 1980.
Manna Z., Pnueli A. Verification of concurrent programs: proving eventualities by well-founded ranking//ACM TOPLAS. Vol.3 1983. P.236-249.
Manna Z., Pnueli A. Verification on concurrent programs: temporal framework/ /The correctness problem in Computer Science. L.: Academic Press. 1981. P.215-273.
Pnueli A. The temporal logic of programs//Proc. 18th IEEE Symposium on the Foundation of Computer Science. San-Francisco, 1977. P.46-57.
Clarke E.f Emerson E. Using branching time logic to synthesize synchronization skeletons//Science of Computing Programming. Vol. 1982. P.241-266.
Emerson E.f Halpem J. "Sometimes" and "not never" revisited: on branching versus linear time//Proc. ACM Symposium on Principles of Programming Languages. Paris, 1983. P.127-140.
Floyd R. Assigning meaning to programs//Proc. of Symposium in Applied Mathematics. N.Y., 1967. P.19-32.
CabbayD., PhueliA., Shelah S., StaviJ. On temporal analysis of fairness //Proc. of ACM Symposium on Principles of Programming Languages. Las-Vegas, 1980. P.163-173.
Kroger F. A generalised nexttime operator in temporal logic / / J. of Computer and System Science. Vol.29. № 1.1984. P.80-98.
Lamport L. "Sometimes" is sometimes "not never" //Proc. of ACM Symposium on Principles of Programming Languages. Las-Vegas, 1980.
Manna Z., Pnueli A. Verification of concurrent programs: proving eventualities by well-founded ranking//ACM TOPLAS. Vol.3 1983. P.236-249.
Manna Z., Pnueli A. Verification on concurrent programs: temporal framework/ /The correctness problem in Computer Science. L.: Academic Press. 1981. P.215-273.
Pnueli A. The temporal logic of programs//Proc. 18th IEEE Symposium on the Foundation of Computer Science. San-Francisco, 1977. P.46-57.