Введение в статический анализ: перспектива абстрактной интерпретации на русском

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

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