Как реализовать символьный механизм выполнения для конкретного языка?

Я рассматриваю возможность использования символического выполнения для проверки надежности программ, написанных на определенном языке, таком как java. Я прочитал несколько статей, в которых представлены основные концепции символического выполнения. Но я не понимаю, как начать.

Например, как я могу сгенерировать условия ограничений из конкретных входных данных? Итак, кто-нибудь может дать мне несколько советов по основам реализации символического выполнения? Кроме того, как насчет конколического исполнения (конкретного + символического)?


person clasnake    schedule 01.11.2013    source источник


Ответы (2)


Возможно, вы можете начать с Symbolic PathFinder http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc

person Ziming Zhao    schedule 15.11.2013

как я могу сгенерировать условия ограничения из конкретного ввода?

используя символьное или конусное исполнение

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

Мой совет такой же, как и у Ziming Zhao: используйте существующий символьный инструмент выполнения. Не пытайтесь реализовать свои собственные, это будет слишком сложно и отнимет много времени.

Вот самые популярные проекты (более полный список здесь):

Java: JPF + Symbolic Pathfinder, JCute.

C и C++: KLEE, Kite

person João Matos    schedule 16.02.2016