?
MicroTESK: Specification-Based Tool for Constructing Test Program Generators
P. 217–220.
В книге
Vol. 10629: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017. , Cham: Springer, 2017.
Shushpanov I., Suslov K., Ilyushin P. и др., Energies 2021 No. 14 Article 6193
Добавлено: 29 декабря 2021 г.
М.: НИУ ВШЭ, 2019.
Учебно-методическое пособие являются составной частью методического обеспечения по дисциплине «Вычислительные системы и компьютерные сети», изучаемой студентами в рамках направления 09.03.01 – «Информатика и вычислительная техника». Основным содержанием является изучение архитектуры компьютера на примере 32-разрядных процессоров Intel и MIPS, их системы команд, последовательности обработки информации при вычислениях с целыми, дробными, символьными данными и числами в двоично-десятичном представлении, ...
Добавлено: 16 ноября 2019 г.
Камкин А. С., Чупилко М. М., Смолов С. А. и др., , in: 2018 19th International Workshop on Microprocessor and SOC Test and Verification (MTV).: Austin: IEEE Computer Society, 2018. P. 6–11.
Добавлено: 3 июля 2019 г.
Камкин А. С., М.: МАКС Пресс, 2018.
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018.
Добавлено: 26 октября 2018 г.
Камкин А. С., Татарников А. Д., Смолов С. А. и др., , in: 2015 16th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2015. P. 1–6.
Добавлено: 18 июля 2018 г.
Камкин А. С., Татарников А. Д., Проценко А. С. и др., , in: 2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2017. P. 10–14.
Добавлено: 18 июля 2018 г.