Описывается трансформация и верификация программы bus_sort_breadthfirst, принадлежащей ядру ОС Linux и реализующей сортировку устройств, прикрепленных к шине компьютера. Программа трансформируется с языка Си в язык cP с раскрытием макросов, реорганизацией структур и устранением указателей. Далее программа преобразуется на язык функционального программирования WhyML. Для полученной программы строится спецификация и проводится дедуктивная верификация.
В статье представлена модель баз данных, основанная на последовательности объектов. Рассмотрены вопросы сериализации/десериализации объектов, индексных построений, структуры и методов универсальной последовательности и универсального индекса, реализация полного базиса редактирования через использование первичного ключа, временной отметки и «пустого» значения.
Показано, что спецификация на языке Event-B представима автоматной программой в виде недетерминировнной композиции простых условных операторов, что соответствует узкому подклассу автоматных программ. Спецификация в Event-B является монолитной. Для построения спецификации нет других средств композиции, кроме уточнения, реализующего расширение ранее построенной спецификации.
Сравнение технологий автоматного программирования и Event-B проводится на примере двух задач. Предыдущие решения задачи управления движением на мосту в системе Event-B являются сложными и громоздкими. Предложено более простое решение с верификацией программы в инструменте Rodin. Эффективность методов верификации в Event-B подтверждена нахождением трех нетривиальных ошибок в нашем решении.
В статье представлены результаты экспериментов по конъюнктивной декомпозиции различных представлений булевых функций (ZDD, BDD, OKFDD, AIG) методами, которые получаются путем специализации общего алгоритма декомпозиции. Тестовыми наборами являются случайные булевы функции с различными параметрами, а также набор широко известных бенчмарков, используемых для тестирования алгоритмов оптимизации логических схем. В сравнении участвуют последовательная и многопоточная реализация алгоритма.