Аннотация:Настоящая статья продолжает опубликованные в № 5, 2015 результаты исследований. На основе анализа публикаций зарубежных и российских авторов с 1990-х годов по настоящее время дана оценка современному состоянию исследований в области формальной верификации программ. Основное внимание при этом уделено подходу к верификации на основе языков программирования с зависимыми типами. Рассмотрены также результаты и на других, смежных направлениях исследований. Обозначены потенциально перспективные, по мнению авторов, направления дальнейших исследований в этой области.