Automatic Formal Verification of Software: Fundamental Concepts

摘要

Formal verification of software is undergoing a renaissance, as highly successful, automatic formal techniques developed for hardware verification are combining with classical software analysis techniques to produce practical, useful tools that scale to large, complicated software. This paper briefly introduces the fundamental concepts behind this renaissance.