Providing means for the development of correct software and the verification of software are central challenges of computer science. This is also the aim of the COMPASS method. It assists in the development of correct code and enables the automatic generation of relevant, focused questions to be asked during code inspection sessions.

COMPASS has been developed within the ISIS project "Verification Automation in Software Development". The project was carried out in cooperation between ABB Industrial Systems and the Real-Time Systems Laboratory at IDA, Linköping University. The COMPASS method is based on Hoare's method for proving programs correct. The novel key idea is the introduction of informal predicates, which, though not having a formal definition, may have a perfectly legal and unique informal interpretation. Such predicates make it easier to express requirements in terms of assertions, while still allowing the automatic generation of verification conditions. Moreover, informal predicates enable reasoning about assertions and verifying verification conditions at a level which is suitable for man rather than machine.

This thesis describes the COMPASS method in detail and reports on preliminary results.