Automated formal analysis and verification: an overview

摘要: This paper provides an overview of various existing approaches to automated formal analysis and verification. The most space is devoted the approach model checking, including its basic principles as well different techniques that have been proposed for dealing with state explosion problem in checking. paper, however, includes a brief discussion theorem proving static too. All discussed are introduced mostly on informal level, attempt provide reader their ideas references works where more details can be found.