Публикации / РИД

Наши статьи

  1. D. Efremov, I. Shchepetkov. Runtime Verification of Linux Kernel Security Module. Proceedings of the 9th International Workshop on Open Community Approaches to Education, Research and Technology, 2020. DOI: 10.1007/978-3-030-54997-8_12.

  2. A. Khoroshilov, V. Kuliamin, A. Petrenko, I. Shchepetkov. A State-based Refinement Technique for Event-B. Proceedings of Ivannikov Memorial Workshop (IVMEM), 2020 (в печати).

  3. И.В. Гладышев, А.С. Камкин, А.М. Коцыняк, П.А. Путро, А.В. Хорошилов. Архитектура системы дедуктивной верификации машинного кода. Труды ИСП РАН, том 32, вып. 3, 2020 г., стр. 7-20. DOI: 10.15514/ISPRAS-2020-32(3)-1.

  4. I. Gladyshev, A. Kamkin, A. Khoroshilov, A. Kotsynyak, P. Putro, I. Gladyshev. Architecture of a Machine Code Deductive Verification System. Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering, 2020.

  5. Р.Ф. Садыков, М.У. Мандрыкин. Верифицированная тактика Isabelle/HOL для теории ограниченных целых на основе инстанцирования и SMT. Труды ИСП РАН, том 32, вып. 2, 2020 г., стр. 107-124. DOI: 10.15514/ISPRAS-2020-32(2)-9.

  6. R. Sadykov, M. Mandrykin. Verified Isabelle/HOL tactic for the theory of bounded linear integer arithmetic based on quantifier instantiation and SMT. Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering, 2020.

  7. P. Andrianov, V. Mutilin. Scalable Thread-Modular Approach for Data Race Detection. Proceedings of the First International Workshop on Frontiers in Software Engineering Education, 2020. DOI: 10.1007/978-3-030-57663-9_24.

  8. P.S. Andrianov. Analysis of Correct Synchronization of Operating System Components. Programming and Computer Software (в печати).

Наши РИД

  1. Программа для ЭВМ "Программный модуль построения, оптимизации и детерминированного воспроизведения доказательств с помощью суперпозиционных решателей и решателей формул в теориях", М.У. Мандрыкин, А.В. Хорошилов, свидетельство о государственной регистрации программы для ЭВМ № 2020661715 от 30.09.20, заявка № 2020660819 от 22.09.20, правообладатель: ИСП РАН, РФ.

  2. Программа для ЭВМ "Программа воспроизведения системных вызовов операционной системы на Event-B модели", Д.В. Ефремов, свидетельство о государственной регистрации программы для ЭВМ № 2020661855 от 01.10.20, заявка № 2020660796 от 22.09.20, правообладатель: ИСП РАН, РФ.

  3. Программа для ЭВМ "Программа генерации монадического представления Си-программ", П.А. Путро, М.У. Мандрыкин, свидетельство о государственной регистрации программы для ЭВМ № 2020661856 от 01.10.20, заявка № 2020660797 от 22.09.20, правообладатель: ИСП РАН, РФ.

  4. Программа для ЭВМ "Программа генерации формальной автоматной модели на основе формализованной модели требований на языке Reka", А.В. Хорошилов, свидетельство о государственной регистрации программы для ЭВМ № 2020661669 от 29.09.20, заявка № 2020660822 от 22.09.20, правообладатель: ИСП РАН, РФ.

Наши монографии

  1. П.Н. Девянин, Д.В. Ефремов, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков. Моделирование и верификация политик безопасности управления доступом в операционных системах. – М.: Горячая линия – Телеком, 2019.

Публикации наших коллег

Для знакомства с основами моделирования и верификации ПО, а также подходами к их инструментальной реализации мы рекомендуем следующие статьи.

  1. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. FRAMA-C, A Software Analysis Perspective // Proceedings of International Conference on Software Engineering and Formal Methods (SEFM), 2012.

  2. Dillon Pariente, Emmanuel Ledinot. Formal Verification of Industrial C Code using Frama-C: a Case Study // Proceedings of First International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), 2010.

  3. Yannick Moy. Automatic Modular Static Safety Checking for C Programs // Phd Thesis, 2009.

  4. Romain Bardou. Verification of Pointer Programs Using Regions and Permissions // Thèse de doctorat, Université Paris-Sud, 2011.

  5. Yannick Moy and Claude Marché. Modular Inference of Subprogram Contracts for Safety Checking // Journal of Symbolic Computation, 2010.

  6. Claude Marché. Verification of the Functional Behavior of a Floating-Point Program: An Industrial Case Study // Science of Computer Programming, 2014.

  7. Ali Ayad. On Formal Methods for Certifying Floating-Point C Programs // Research Report RR-6927, INRIA, 2009.

  8. Sylvie Boldo. Floats and Ropes: A Case Study for Formal Numerical Program Verification // Proceedings of 36th Internatilonal Colloquium on Automata, Languages and Programming (ICALP), 2009.

  9. Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-Independent Proofs of Numerical Programs // Proceedings of the Second NASA Formal Methods Symposium, 2010.

  10. Mickaël Delahaye, Nikolai Kosmatov, and Julien Signoles. Common Specification Language for Static and Dynamic Analysis of C Programs // Proceedings of the 28th Annual ACM Symposium on Applied Computing (SAC), 2013.