Extending the Reach and Power of Deductive Program Verification

Software is vital for modern society. The efficient development of correct and reliable software is of ever-growing importance. An important technique to achieve this goal is deductive program verication: the construction of logical proofs that programs are correct. In this thesis, we address three important challenges for deductive verication on its way to a wider deployment in the industry: 1. verication of thread-based concurrent programs 2. correctness management of verication systems 3. change management in the verication process. These are consistently brought up by practitioners when applying otherwise mature verication systems. The three challenges correspond to the three parts of this thesis (not counting the introductory rst part, providing technical background on the KeY verication approach). In the first part, we dene a novel program logic for specifying correctness properties of object-oriented programs with unbounded thread-based concurrency. We also present a calculus for the above logic, which allows verifying actual Java programs. The calculus is based on symbolic execution resulting in its good understandability for the user. We describe the implementation of the calculus in the KeY verication system and present a case study. In the second part, we provide a systematic survey and appraisal of factors involved in reliability of formal reasoning. We elucidate the potential and limitations of self-application of formal methods in this area and give recommendations based on our experience in design and operation of verication systems. In the third part, we show how the technique of similarity-based proof reuse can be applied to the problems of industrial verication life cycle. We address issues (e.g., coping with changes in the proof system) that are important in verication practice, but have been neglected by research so far.