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