Новости

23.08.2021: Поиск ошибок использования памяти в ядре Linux

Лутовинова Надежда завершила проект GSoC “Поиск ошибок, связанных с памятью, в ядре Linux и улучшение спецификации модели окружения для статической верификации”. Этот проект был связан с поиском ошибок, связанных с памятью, в коде драйверов Linux. В процессе работы Надежда использовала Klever - фреймворк для верификации программного обеспечения, созданный для автоматической проверки программ, написанных на языке программирования C. С помощью него она анализировала код ядра Linux версии 5.12-rc3.

20.08.2021: Анализ и исправление состояний гонок в ядре ОС Linux

Saubhik Mukherjee успешно завершил GSoC 2021 “Анализ и исправление ошибок, связанных с состояниями гонки, в ядре ОС Linux” под эгидой The Linux Foundation. Его основная задача заключалась в поиске ошибок, связанных с состоянием гонки в драйверах операционной системы Linux версии 5.4. Статическая верификация проводилась с помощью инфраструктуры Klever. С помощью веб-интерфейса полученные трассы ошибок анализировались и классифицировались на реальные ошибки и ложные предупреждения.

31.08.2020: Разработка спецификаций модели окружения для статической верификации ядра ОС Linux

Лутовинова Надежда закончила проект GSoC 2020 “Разработка спецификаций модели окружения для статической верификации ядра Линукс” под эгидой The Linux Foundation.

28.08.2020: Анализ и исправление состояний гонок в ядре ОС Linux

Madhuparna Bhowmik успешно завершила проект GSoC 2020 “Анализ и исправление ошибок, связанных с состояниями гонки, в ядре ОС Linux” под эгидой The Linux Foundation. Проект включал в себя использование интерфейса Клевер для поиска ошибок, связанных с некорректной синхронизацией потоков, в ядре ОС Linux v4.18. Большая их часть все еще присутствовала в последней версии ядра v5.9.

04.10.2019: На острове Фрауэнкимзе прошел семинар CPA&LDV Workshop

Семинар CPA&LDV Workshop прошел на острове Фрауэнкимзе, Германия с 1 по 2 октября, 2019 года.

06.04.2019: CPAchecker-BAM-BnB и CPALockator на SV-COMP'2019

На международных соревнованиях инструментов статической верификации (SV-COMP 2019), проходивших в рамках международной конференции TACAS, Прага, Чехия, были представлены доклады по инструментам CPAchecker-BAM-BnB и CPALockator. В этом году наш инструмент CPAchecker-BAM-BnB завоевал золотую медаль в категории Software Systems, а CPALockator участвовал в категории Concurrency Safety.

27.09.2018: В Москве прошел семинар CPA&LDV Workshop

25-26 сентября 2018 года в Москве прошел седьмой международный семинар CPA&LDV Workshop.

13.08.2018: Улучшение модели окружения для задач верификации ядра ОС Linux на корректность использования памяти и поиск ошибок использования памяти в ядре ОС Linux

Антон Васильев закончил проект "Улучшение модели окружения для задач верификации ядра ОС Linux на корректность использования памяти и поиск ошибок использования памяти в ядре ОС Linux", выполненный в рамках Google Summer of Code 2018 под эгидой The Linux Foundation.