Проблемы параметризованной верификации протоколов когерентности памяти
11
[15] Emerson A., Namjoshi K. Reasoning about Rings.
Proceedings of the 22nd
ACM SIGPLAN-SIGACT symposium on Principles of programming lan-
guages
, 1995, pp. 85–94.
[16] Clarke E., Talupur M., Touili T., Veith H. Verification by Network Decompo-
sition.
CONCUR
, 2004, vol. 3170, pp. 276–291.
[17] Park S., Dill D. Verification of FLASH Cache Coherence Protocol by Aggre-
gation of Distributed Transactions.
Proceedings of the 8th annual ACM sym-
posium on parallel algorithms and architectures,
1996, pp. 288–296.
[18] Owre S., Rushby J., Shankar N. PVS: A prototype verification system.
Auto-
mated Deduction
, 1992, vol. 607, pp. 748–752.
[19] Kuskin J., Ofelt D., Heinrich M., Heinlein J., Simoni R., Gharachorloo K., Cha-
pin J., Nakahira D., Baxter J., Horowitz M., Gupta A., Rosenblum M., Hen-
nessy J. The Stanford FLASH multiprocessor.
ISCA Proceedings of the 21st an-
nual international symposium on Computer architecture
, 1994, pp. 302–313.
[20] McMillan K. Parameterized Verification of the FLASH Cache Coherence Pro-
tocol by Compositional Model Checking.
Proceedings of the 11th IFIP WG
10.5 Advanced Research Working Conference on Correct Hardware Design
and Verification Methods
, 2001, pp. 179–195.
[21] Krstic S.
Parameterized System Verification with Guard Strengthening and
Parameter Abstraction. Automated Verification of Infinite State Systems,
2005.
[22] Talupur M., Tuttle M. Going with the Flow: Parameterized Verification Using
Message Flows.
Formal Methods in Computer-Aided Design
, 2008, pp. 1–8.
[23] Talupur M., Krstic S., O’Leary J., Tuttle M.R. Parametric Verification of In-
dustrial Strength Cache Coherence Protocols.
In Proc. Workshop on Design of
Correct Circuits (DCC),
2008.
[24] Bingham J. Automatic Non-interference Lemmas for Parameterized Model
Checking.
Formal Methods in Computer-Aided Design
, 2008, pp. 77–85.
Статья поступила в редакцию 28.06.2013
Ссылку на эту статью просим оформлять следующим образом:
Буренков В.С., Иванов С.Р. Проблемы параметризованной верификации прото-
колов когерентности памяти.
Инженерный журнал: наука и инновации,
2013, вып. 11.
URL:
Буренков Владимир Сергеевич
родился в 1989 г., окончил МГТУ им. Н.Э. Ба-
умана в 2012 г. Аспирант МГТУ им. Н.Э. Баумана. Автор более семи научных ра-
бот. Области научных интересов: формальная верификация вычислительных си-
стем, алгоритмы и структуры данных, архитектура микропроцессорных систем. e-
mail:
Иванов Сергей Ростиславович
родился в 1937 г. Окончил МВТУ им. Н.Э. Ба-
умана в 1960 г. Канд. техн. наук, доцент кафедры «Компьютерные системы и сети»
МГТУ им. Н.Э. Баумана. Автор более 60 научных работ. Область научных интере-
сов: системы автоматизированного проектирования электронных схем. e-mail:
