ДЕТЕРМИНИРОВАННЫЙ АЛГОРИТМ АНАЛИЗА КОДА ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ

Илья Викторович Арзамарцев, Георгий Иванович Борзунов

Аннотация


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

Ключевые слова


символьное исполнение; статический анализ; верификация кода

Полный текст:

PDF

Литература


1 King J. C. Symbolic Execution and Program Testing // Magazine Communications of ACM. 1976. Vol. 19. P. 385-394.

2 Арзамарцев И. В., Юров И. А. Метод анализа зависимостей между входными и выходными данными алгоритмов // Безопасность информационных технологий. 2013. № 2. С. 18-22.

3 Carette J., Janicki R., Zhai Y. Program verification by calculating relations // Conference of Applied Simulation and Modeling. 2006. Track 522-112.

4 Sang Kil Cha, Avgerinos T., Rebert A., Brumley D. Unleashing Mayhem on Binary Code // Proceedings of the 2012 IEEE Symposium on Security and Privacy. P. 380-394.

5 Babic D., Martignoni L., McCamant S., Song D. Statically-directed dynamic automated test generation // Proceedings of the 2011 International Symposium on Software Testing and Analysis. P. 12-22.


Ссылки

  • На текущий момент ссылки отсутствуют.


Лицензия Creative Commons
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.