Найден способ формального подтверждения 100% отсутствия ошибок в программе
 

Ученые из австралийского исследовательского центра NICTA нашли способ математически доказать, что определенное ПО не содержит ошибок и, соответственно, не станет причиной отказа управляемого им оборудования. Проведение такого рода тестирования жизненно необходимо во многих отраслях промышленности, таких как, например, авиа и автомобилестроение, где сбои в бортовой компьютерной сети возникают чаще, чем поломки механических агрегатов.
Для проведения теста было взято микроядро Secure Embedded L4 (seL4), содержащее 8700 строк кода базирующегося на open source проекте OKL4. Ядро является ключевым компонентом любых современных встраиваемых устройств, и имеет неограниченный доступ ко всем работающим системам. Суть тестирования заключалась в том, чтобы доказать, что написанный код удовлетворяет всем тем спецификациям, которые были заложены на этапе проектирования. В результате, испытание было пройдено успешно и достигнуто 100% соответствие предъявляемым требованиям.
Работой по формулировке алгоритма математического доказательства в течение четырех лет занималась команда из 12 исследователей NICTA, аспирантов и техников. Они успешно проверили более 10 тыс. промежуточных теорем, изучив более чем 200 тыс. строк кода. Итоговый анализ выполняется с помощью интерактивной программы Isabelle, и на сегодняшний день является самой объемной автоматизированной проверкой выполнения условий теорем.
Наряду с доказательством соответствия программного кода выполняемым функциям, тестирование показало, что seL4 не подвержен большинству известных хакерских атак. Например, атака «переполнение буфера», позволяющая внедрить злонамеренный код и захватить управление работой ядром, не даст результата.
Полное изложение работы исследователей будет озвучено на 22-ом симпозиуме, посвященном принципам работы операционных систем (SOSP). Также ожидается, что NICTA передаст все интеллектуальные права на результаты исследования opensource компании Open Kernel Labs.
14.08.2009

вот полное изложение работы и будет показателем правдивости журналистов. Мне кажется, что они создали очень узкоспециализированый модуль, который мало к чему можно применить. Моль, ИИ по твоей части.

нужно пытаться доказывать не то что оно правильно работает, а наоборот, то что оно неправильно работает

Да ладно вам, я нисколько не сомневаюсь что это уже доказано.

8700 строчек кода не так сложно "вылизать". Зачет за такой опен-сорс проект.

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

На самом деле формулировка очень общая. Cthulchu прав, что нужно более информации, чтобы судить. И дело тут вовсе не в механизмах доказательств алгоритмов, imho, он давно известен и применяется, дело в самой системе, а точнее ядре и её полному соответствию предъявляемым требованиям..

опять журналюги что-то мутят - ничего, что ещё Тьюринг доказал, что нет алгоритма, определяющего, зависнет ли заданный алгоритм на заданных входных данных (http://en.wikipedia.org/wiki/Halting_problem, например). Или это не считается ошибкой в программе? *или речь вообще о синтаксисе идёт?:)

А если сама их программа даст сбой ))

Вот насчет этого уже думаю сомневаться не стоит)