Анализ потоков данных. Связь MOP-, MFP-, ideal-решений. Абстрактная интерпретация. Понятие решётки. Понятия конкретного и абстрактного состояний. Связь абстрактной интерпретации и анализа потока данных. Вычисление необходимых условий для поиска переполнения буфера. Понятия полноты и корректности. Примеры абстракций: интервальная абстракция, предикатная абстракция. SMT-решатели.