Integration of Verification Methods for Program Systems

摘要

In the paper, an approach to constructing an extensible framework for the verification of program systems is suggested. In the author's opinion, it will facilitate application of modern rigorous verification methods to practically significant programs, the complexity of which permanently grows. This framework can also become a test harness for testing and adjustment of new techniques of formal verification and static analysis on various industrial software packages.