Предвидение сбоев программы

Question

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

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

Коллега сказал, что то, что я пытаюсь сделать, принципиально невозможно.Это кажется мне немного экстремальным.Принимая во внимание закономерность развития технологий, предложенную Муром, вычислительная мощь, находящаяся за пределами досягаемости, в конечном итоге станет реальностью - в конце концов.Было бы немного преувеличением предположить, что такая вещь останется навсегда невозможной .

Почему этого нельзя сделать?

Answer 1

Вот программа:

accept integer i greater than 2
loop with k from 2 to 2*i
  is k prime?
    is 2*i-k prime?
      exit safely
end loop
do something nasty.

Если вы отслеживаете ввод, который заставляет эту программу делать что-то неприятное, вы решили гипотеза Гольдбаха .Вы можете получить медаль Поля вместе с вашим Нобелевским призом.

При этом можно проверить, что некоторые программы не делают ничего противного.Я и другие работаем над фреймворком, в котором вы можете сделать это, используя различные методы .Некоторые примеры:

Эта библиотека сжатия может показывать ошибку памяти с размером ввода 20, размером вывода 40, но теперь этого не происходит.

Этот двоичный файлпоиск может быть неудачным, но теперь это не так.

Answer 2

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

Да, это возможно, несмотря на то, что говорят теоретики. Есть несколько компаний, продающих продукты, которые делают именно то, что вы описываете, среди них Vericode, Coverity, Fortify, Klocwork и Grammatech.

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

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

Редактировать, для комментария Алекса
Я возьму ярлык математики и скажу, что поскольку первоначальный вопрос «Возможно ли», существование нескольких жизнеспособных коммерческих продуктов доказывает, что ответ «да». Экономические зависимости, которые могут быть созданы с помощью коммерческого программного обеспечения, выходят за рамки первоначального вопроса.

Answer 3

Это один из священных Граалей вычислительной техники и математики, известный как Entscheidungsproblem .Вы не собираетесь это решить.Самые яркие умы в обеих областях потратили много лет на это, и доказали, что это не может быть решено.Когда Нбт и Паскаль Куок сказали, что вы выиграете Нобелевскую и Полевую премию за это, они действительно это имели в виду.