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

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
Main Authors: Aleksandr V. Misonizhnik, Yurii O. Kostyukov, Michael P. Kostitsyn, Dmitry A. Mordvinov, Dmitry V. Koznov
Format: Article
Language:English
Published: Saint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University) 2022-10-01
Series:Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki
Subjects:
weakest preconditions
symbolic execution
backward symbolic analysis
bidirectional analysis
automatic test generation
Online Access:https://ntv.ifmo.ru/file/article/21527.pdf

Internet

https://ntv.ifmo.ru/file/article/21527.pdf

Similar Items