THE INTEGRATED SOFTWARE-DEVELOPMENT AND VERIFICATION SYSTEM ATES

This paper is a project report, presenting a few results of the ESPRIT project ATES, concerned with formal software development. A programming and proof system, based on a high level, abstract language, able to express the specifications necessary to develop reliable software, in a program-to-proof approach is described. Within this approach, we want to conceive a program and introduce the elements necessary for its proof, at the same time. (Those formal proof elements consist in logical assertions expressing mathematically what an algorithm does and logical properties of the function realized by the algorithm). Those proof elements will be used by the system, to verify the correctness of an algorithm, guided by an interactive proof checker.