Grant: Discovery Grants Program - Individual

Every user of computer systems is familiar with errors and/or misbehavior of software products. This is an annoying situation but for most applications not serious. On the other hand, especially in the area of ebusiness correct programs become more and more important. For example, every user of such a program wants to be sure that secret data (credit card number, pin, etc.) are not accessible to unauthorized persons. Another example might be software controlling a nuclear plant. It is desirable that such a program does not fail. One method for developing reliable software products is program verification, i.e. providing a mathematical proof of correctness versus a given specification. For the reasons mentioned above a certification of a software product following the European ITSEC (Information Technology Security Evaluation Criteria) at level E4-E6 - the three highest certification/assurance levels of that standard - requires the application of formal methods including correctness proofs of at least parts of the system. The existing tools and methods are very limited in providing mechanisms to transfer properties, their proofs and proof methods from one construction to another. One is forced to start on a very basic level, which generates a huge amount of proof obligations. In real world examples proving all obligations is often not feasible or at least too expensive. A system and its underlying methodology, which allows less expensive development of verified programs would be of great benefit for software developers and finally for all users. My objective is to establish such a system and methodology, and, thus, to transfer theoretical results to real world applications. The overwhelming success of object-oriented programming languages is based on reuse of software components. I will apply the same idea to the corresponding proof system. Properties of programs and their proof will be integrated into the class hierarchy such that a suitable inheritance mechanism transfers operations as well as the related properties and proofs to subclasses.