Извините, регистрация закрыта. Возможно, на событие уже зарегистрировалось слишком много человек, либо истек срок регистрации. Подробности Вы можете узнать у организаторов события.
In the first part a brief overview will be given on Autoproof tool, that is an automated verifier for the Eiffel programming language. It proves functional correctness of Eiffel programs annotated with contracts. In the second part we will discuss Tokeneer project implemented in Eiffel language and proving it with Autoproof tool. Tokeneer is a research work for NSA done in 90-s, that has now been made available to the software development and security communities in an effort to prove that it is possible to develop secure systems rigorously in a cost effective manner. It became some kind of “milestone in the transfer of software verification technology into industrial application”.
In the first part a brief overview will be given on Autoproof tool, that is an automated verifier for
the Eiffel programming language. It proves functional correctness of Eiffel programs annotated with
contracts.
In the second part we will discuss Tokeneer project implemented in Eiffel language and proving it
with Autoproof tool. Tokeneer is a research work for NSA done in 90-s, that has now been made
available to the software development and security communities in an effort to prove that it is
possible to develop secure systems rigorously in a cost effective manner. It became some kind of
“milestone in the transfer of software verification technology into industrial application”.