Рассмотрена задача повышения рентабельности алгоритмов статического анализа. Ключевой проблемой формальных методов верификации является избыточность исходного текста программы для верификации конкретного ее свойства. В этой связи возникает необходимость элиминации избыточного кода. Эта задача, как и задачи исследования свойств программы, решается с использованием консервативных методов. Показано, как избыточная консервативность снижает рентабельность сертификации такого программного обеспечения. Предложен и алгоритмически реализован метод снижения консервативности алгоритмов статического анализа на примере алгоритма поиска достигающих определений.

  Якщо, ви не знайшли інформацію про автора(ів) публікації, маєте бажання виправити або відобразити більш докладну інформацію про науковців України запрошуємо заповнити "Анкету науковця"