7 posts
Ваши модульные тесты проверяют конкретные входные данные. Символическое исполнение проверяет каждый возможный ввод. Вот как это работает, чего это стоит и с чего начать.
У вашего набора тестов 94% покрытия и ноль падений. Движок символического исполнения находит краш в вашем коде менее чем за три секунды. Тесты не сломаны.…
Абстрактная интерпретация позволяет доказать невозможность ошибок времени выполнения ещё до запуска программы. Вот как это работает на самом деле, почему это сложно и где это применяется в вашем инструментарии.
Ваш набор тестов проходит. Ваш type checker зелёный. Вы выкладываете в прод. Через два часа продакшен выдаёт на граничном случае, который никому не пришло в…
Cleanroom software engineering обещала инкременты с нулевым количеством дефектов через mathematical verification вместо debugging. Мы смотрим на реальные данные проекта IBM, чтобы проверить, выдержал ли этот тезис.
Среднее значение по индустрии программного обеспечения в 1980-х годах составляло от 30 до 60 дефектов на тысячу строк кода. Команда Cleanroom в IBM поставила…
AutoVerus использует сеть агентов LLM для генерации proof корректности Verus для кода на Rust, автоматизируя более 90% proof obligations через цикл generate-repair-discharge, управляемый обратной связью SMT-solver.
Самая сложная часть формальной верификации никогда не заключалась в verifier. Она заключается в написании proof. Дайте опытному инженеру по Rust Verus —…
Bounded model checkers вроде Kani и реляционные model finders вроде Alloy позволяют проверять свойства с помощью обычных assertions и constraints. Вы жертвуете доказательствами liveness ради кривой обучения, измеряемой часами, а не неделями.
Не нужно изучать линейную темпоральную логику, чтобы использовать model checker. Инструменты вроде Kani, CBMC и Alloy позволяют проверять свойства с помощью…
Инструменты model checking вроде Kani позволяют верифицировать свойства Rust с помощью assertions вместо формальных доказательств. Проблема в том, что происходит, когда ваши циклы не имеют маленьких границ.
Можно доказать корректность кода на Rust, не написав ни одного доказательства. Инструмент, который это делает, называется model checker, а для Rust наиболее…
N-версионное программирование предполагает, что ваши реализации согласованы. Мы разбираем, почему тестов недостаточно, как SMT-солверы могут реально доказать эквивалентность и где провести границу между «достаточно хорошо» и формально верифицировано.
Вы построили n-версионную систему. Три независимые реализации одной и той же критической функции, voter, который выбирает результат большинства, и приятное…