Generation of the weakest preconditions of programs with dynamic memory in symbolic execution

Symbolic execution is a widely used method for the systematic study of program execution paths; it allows solving a number of important problems related to verification of correctness: searching for errors and vulnerabilities, automatic test generation, etc. The main idea of symbolic execution is ge...

Full description

Bibliographic Details

Published in:	Научно-технический вестник информационных технологий, механики и оптики
Main Authors:	A. V. Misonizhnik, Yu. O. Kostyukov, M. P. Kostitsyn, D. A. Mordvinov, D. V. Koznov
Format:	Article
Language:	English
Published:	ITMO University 2024-12-01
Subjects:	слабейшие предусловия символьное исполнение обратный символьный анализ двунаправленный анализ автоматическая генерация тестов
Online Access:	https://ntv.elpub.ru/jour/article/view/82