В МТИ предложен метод защиты программ от ошибок, основанный на теории управления Ляпунова
Источник: MIT News

Они названы так по имени великого русского математика и являются одной из основ теории управления. Простейший пример функции Ляпунова описывает движения маятника.

Авторы предлагают рассматривать компьютерную программу как набор правил перемещения в пространстве, определенном переменными программы и размещением в памяти ее команд. Любое состояние программы — набор значений переменных при выполнении очередной инструкции — точка такого пространства. Критические ошибки исполнения, например, деление на ноль или переполнение памяти, можно рассматривать как области этого пространства.

В таком контексте задача формальной верификации сводится к демонстрации того, что программа никогда не «заведет» свои переменные в зоны критических ошибок. Для этого исследователи предложили аналог функций Ляпунова, которые они назвали инвариантами Ляпунова. График функции Ляпунова похож на чашу, ее нижняя точка — состояние максимальной стабильности. Для программы нужно найти такой инвариант Ляпунова, чтобы начальные значения переменных находились на дне «чаши», а все опасные зоны — выше на стенках. В этом случае попадание в опасную зону будет равносильно тому, что маятник качнулся сильнее, чем в предыдущий раз.