PhD, профессор
заведующий кафедрой программной инженерии ETH
профессор университета Иннополис
основатель, исполнительный директор и старший архитектор Eiffel Software

It is possible today to write advanced object-oriented programs and prove them correct as part of a normal development process. I will present the AutoProof interactive development and verification and system, based on Eiffel, which has already been used to verify significant OO programs making full use of a modern language. I will explain the concepts, present the tool in an interactive demo, and describe limitations and future developments.