Система автоматического поиска инварианта цикла

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