Verification of large software systems

Abstract

This paper presents a formal approach to the specification, construction and automated verification of large software systems. We describe the design methodology, the theory of correctness, the proof strategy for the resulting proof obligations, and the experiences from case studies carried out using the Karlsruhe Interactive Verifier (KIV). The design methodology supports the top-down development of structured algebraic first-order specifications and stepwise implementation of its parts by program modules. The correctness of the resulting modular systems is proved to be compositional. For the correctness of single program modules we give a characterization in terms of Dynamic Logic. This provides a general solution to the correctness problem for implementations of full first-order specifications.