студент, 630090, Россия, г. Новосибирск, ул. Пирогова, 2
студент, ul. Pirogova, 2, Novosibirsk, 630090, Russia
ст. науч. сотр., 630090, Россия, г. Новосибирск, пр. Лаврентьева, 6
ст. науч. сотр., Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia
По сравнению с традиционным тестированием дедуктивная верификация предлагает более формальный способ доказательства корректности программ. Но как установить корректность самой системы верификации? Теоретические основы логик Хоара исследовались в классических работах, где были получены различные результаты по непротиворечивости и полноте. Однако нам не известны реализации этих теоретических методов, проверенные чем-либо отличным от обычного тестирования. Иными словами, нас интересует система верификации, которая может быть применена к самой себе (хотя бы частично). В наших исследованиях мы обратились к методу метагенерации, который выглядит многообещающим для этой задачи.
As opposed to traditional testing, the deductive verification represents a formal way to examine the program correctness. But what about the correctness of the verification system itself? The theoretical foundations of Hoare’s logic were examined in classical works, and some soundness/completeness theorems are well-known. However, we practically are not aware of implementations of those theoretical methods which were subjected to anything more than testing. In other words, our ultimate goal is a verification system which can be self-applicable (at least partially). In our recent studies we addressed ourselves to the metageneration approach in order to make such a task more feasible.
The authors declare that there are no conflicts of interest present.