Информатика и системы управления
 
 
 
 
 
 
 
 
 
 
 
 
 
 
Другие журналы

электронный журнал

МОЛОДЕЖНЫЙ НАУЧНО-ТЕХНИЧЕСКИЙ ВЕСТНИК

Издатель Академия инженерных наук им. А.М. Прохорова. Эл No. ФС77-51038. ISSN 2307-0609

Подходы к верификации протоколов когерентности памяти

Молодежный научно-технический вестник # 08, август 2013
УДК: 004.052.4
Файл статьи: Буренков В.С..pdf (105.48Кб)
автор: Буренков В. С.

1.       Pong F., Dubois M. A New Approach for the Verification of Cache Coherence Protocols // IEEE Transactions on Parallel and Distributed Systems. 1995. Vol. 6, Issue 8, pp. 773-787.

2.       Буренков В.С. Метод перебора состояний для верификации протоколов когерентности памяти. // 54-я научная конференция МФТИ, 2011.

3.       Pong F., Dubois M. Verification Techniques for Cache Coherence Protocols // ACM Computing Surveys. 1997. Vol. 29, Issue 1, pp. 82-126.

4.       Clarke E., Grumberg O., Peled D. Model Checking. MIT Press, 1999. 314 pp.

5.       Chou C., Mannava P., Park S. A Simple Method for Parameterized Verification of Cache Coherence Protocols // Formal Methods in Computer-Aided Design. 2004. Vol. 3312, pp. 382-398.

6.       Harrison J. Formal Methods at Intel – An Overview // Second NASA Formal Methods Symposium, 2010.

7.       Буренков В.С. Инструмент верификации протокола когерентности памяти // Молодежный научно-технический вестник. 2013. № 1.

8.       O’Leary J., Talupur M., Tuttle M. Protocol Verification Using Flows: An Industrial Experience // Formal Methods in Computer-Aided Design. 2009. pp. 172-179.

9.       Apt K., Kozen D. Limits for Automatic Program Verification of Finite-State Concurrent Systems // Information Processing Letters. 1986. Vol. 22, Issue 6, pp. 307-309.

10.   Emerson A., Kahlon V. Reducing Model Checking of the Many to the Few // Automated Deduction. 2000. Vol. 1831. pp. 236-254.

11.   Emerson A., Kahlon V. Model Checking Large-Scale and Parameterized Resource Allocation Systems // Tools and Algorithms for the Construction and Analysis of Systems. 2002. Vol. 2280. pp. 251-265.

12.   Emerson A., Namjoshi K. Reasoning about Rings. // Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 1995. pp. 85-94.

13.   Clarke E., Talupur M., Touili T., Veith H. Verification by Network Decomposition // CONCUR. 2004. Vol. 3170. pp. 276-291.

14.   Clarke E., Talupur M., Veith H. Environment Abstraction for Parameterized Verification // Verification, Model Checking, and Abstract Interpretation. 2006. Vol. 3855. pp. 126-141.

15.   Talupur M. Abstraction Techniques for Parameterized Verification // PhD Thesis. 2006.

16.   Clarke E., Talupur M., Veith H. Proving Prolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems // Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems. 2008. pp. 33-47.

17.   Park S., Dill D. Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions // Proceedings of the eighth annual ACM symposium on parallel algorithms and architectures. 1996. pp. 288-296.

18.   Owre S., Rushby J., Shankar N. PVS: A prototype verification system // Automated Deduction. 1992. Vol. 607. pp. 748-752.

19.   Kuskin J., Ofelt D., Heinrich M., Heinlein J., Simoni R., Gharachorloo K., Chapin J., Nakahira D., Baxter J., Horowitz M., Gupta A., Rosenblum M., Hennessy J. The Stanford FLASH multiprocessor // ISCA Proceedings of the 21st annual international symposium on Computer architecture. 1994. pp. 302-313.

20.   McMillan K. Parameterized Verification of the FLASH Cache Coherence Protocol 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. 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.   Abts D., Scott S., Lilja D. So Many States, So Little Time: Verifying Memory Coherence in the Cray X1 // Proceedings of the 17th International Symposium on Parallel and Distributed Processing. 2003.

24.   Qin X. Mishra P. Automated Generation of Directed Tests for Transition Coverage in Cache Coherence Protocols // Design, Automation & Test in Europe Conference & Exhibition. 2012. pp. 3-8.


Тематические рубрики:
Поделиться:
 
ПОИСК
 
elibrary crossref neicon rusycon
 
ЮБИЛЕИ
ФОТОРЕПОРТАЖИ
 
СОБЫТИЯ
 
НОВОСТНАЯ ЛЕНТА



Авторы
Пресс-релизы
Библиотека
Конференции
Выставки
О проекте
Rambler's Top100
Телефон: +7 (499) 263-61-98
  RSS
© 2003-2024 «Молодежный научно-технический вестник» Тел.: +7 (499) 263-61-98