23.09.2015: В Москве состоялся пятый Linux Driver Verification Workshop

user warning: Got error 28 from storage engine query: SELECT t.*,v.weight AS v_weight_unused FROM term_node r INNER JOIN term_data t ON r.tid = t.tid INNER JOIN vocabulary v ON t.vid = v.vid WHERE r.vid = 256 ORDER BY v.weight, t.weight, t.name in /opt/drupal-6.33/modules/taxonomy/taxonomy.module on line 640.

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) в направлении получения доказательств без ограничений на количество итераций.

В заключении команды обсудили открытые вопросы и согласовали задачи по направлениям дальнейшего развития.