23.09.2015: В Москве состоялся пятый Linux Driver Verification Workshop
15-18 сентября 2015 года в Москве состоялся пятый международный семинар Linux Driver Verification посвященный десятой годовщине Центра Верификации ОС Linux. Семинар был организован проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН, Москва, Россия) и проф. Дирком Бейером (Dirk Beyer, Университет г. Пассау, Германия).
Алексей Хорошилов открыл 5-ый семинар Linux Driver Verification и рассказал об основных достижениях инструмента CPAchecker в рамках его использования в проекте Linux Driver Verification. Он заключил, что BLAST все еще полезен как вспомогательный инструмент, но CPAchecker наконец стал основным инструментом верификации в проекте LDV.
Дирк Бейер (Dirk Beyer) представил доклад "Witness Validation and Stepwise Testification across Software Verifiers", в котором он описал методы проверки результатов одного инструмента верификации другими инструментами верификации. Также он продемонстрировал преимущества в сокращении множества перебираемых состояний и возможности для эффективных комбинаций различных техник верификации.
Ускорение за счет последовательных комбинаций различных подходов было продемонстрировано Вадимом Мутилиным. Он выявил несколько конфигураций, в которых CPAchecker имеет результаты на драйверах устройств лучше, чем текущая конфигурация. В докладе он обсудил текущее состояние использования инструмента CPAchecker без CIL и проблемы недетерминированного поведения.
Виталий Мордань описал подход, позволяющий проверять одновременно несколько свойств, который значительно ускоряет анализ с результатами, практически полностью идентичными подходу, проверяющему свойства последовательно одно за другим.
Адреас Стахлбауэр (Andreas Stahlbauer) сделал доклад "Multi-Property Verification Using Precision Control", в котором обсуждались проблемы, обозначенные Виталием, с акцентом на формализацию в контексте Configurable Program Analysis (CPA). Он заключил, что затраты на проверку не обязательно сильно увеличиваются при растущем количестве проверяемых свойств.
В дополнение Виталий сделал доклад на тему "Finding Several Bugs at Once", в котором описывался похдод, не останавливающийся после нахождения первого нарушения, а напротив, продолжал находить другие нарушения того же свойства пока не найдутся все имеющиеся. Данный подход сопровождается невероятным количеством трасс ошибок, относящихся к одинаковым ошибкам. Поэтому Виталий представил метод кластеризации трасс ошибок, позволяющий снизить затраты на их анализ.
Павел Андрианов обсудил проблемы и перспективы Block Abstraction Memorization (BAM). Проблемы были связаны с такими частями BAM как построение разбиения на блоки, вычисление пути, очистка ARG, агрессивная редукция предикатов и т.д.
В докладе "Theory-Independent Reuse of Abstraction Formulas: Towards Proof Reuse" Карлхайнц Фредбергер (Karlheinz Friedberger) преставил подходы по переиспользованию формул в анализах, использующих линейную арифметику и битовые векторы, а также способы преобразования между ними с целью ускорения верификации программ с битовой точностью.
Себастиан Отт (Sebastian Ott) представил доклад "A Web-Interface for the CPAchecker Cloud" об облаке, позволяющем параллельную верификацию большого количества заданий с точными и воспроизводимыми результатами. Это облако успешно используется при разработке инструмента CPAchecker и существенно ускоряет цикл разработки-тестирования.
Антон Васильев рассказал о проверке безопасного использования памяти для ядра ОС Linux. Он выявил ряд проблем в имеющемся подходе SMGCPA, использовавшемся на Международных соревнованиях по верификации программ (SV-COMP'15) и предложил потенциальные решения.
Илья Захаров исследовал узкие места производительности инструмента CPAchecker на драйверах устройств ОС Linux и представил результаты экспериментов, а также классификацию проблем для различных конфигураций CPAchecker. Михаил Мандрыкин рассказал о направлениях по улучшению модели памяти в инструменте CPAchecker. Виталий Мордань подготовил результаты первых экспериментов со сложными спецификациями, реализованными в виде свойств-автоматов в инструменте CPAchecker.
Дирк Бейер (Dirk Beyer) сделал доклад "Boosting k-Induction with Continuously-Refined Invariants", в котором представил подход, расширяющий возможности Bounded Model Checking (BMC) в направлении получения доказательств без ограничений на количество итераций.
В заключении команды обсудили открытые вопросы и согласовали задачи по направлениям дальнейшего развития.
