Towards the ’Verified Verifier’. Theory and Practice
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 t...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2014-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/72 |
| _version_ | 1797877954273869824 |
|---|---|
| author | D. A. Kondratyev A. V. Promsky |
| author_facet | D. A. Kondratyev A. V. Promsky |
| author_sort | D. A. Kondratyev |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-10T02:24:57Z |
| format | Article |
| id | doaj.art-7714fc9a1e834e80aee06df037fb1fe4 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:24:57Z |
| publishDate | 2014-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-7714fc9a1e834e80aee06df037fb1fe42023-03-13T08:07:32ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172014-12-01216718210.18255/1818-1015-2014-6-71-8266Towards the ’Verified Verifier’. Theory and PracticeD. A. Kondratyev0A. V. Promsky1Новосибирский государственный университетИнститут систем информатики имени А.П. Ершова СО РАН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.https://www.mais-journal.ru/jour/article/view/72верификацияспецификацияаксиоматическая семантикаязык c-lightусловие корректностиметагенерация |
| spellingShingle | D. A. Kondratyev A. V. Promsky Towards the ’Verified Verifier’. Theory and Practice Моделирование и анализ информационных систем верификация спецификация аксиоматическая семантика язык c-light условие корректности метагенерация |
| title | Towards the ’Verified Verifier’. Theory and Practice |
| title_full | Towards the ’Verified Verifier’. Theory and Practice |
| title_fullStr | Towards the ’Verified Verifier’. Theory and Practice |
| title_full_unstemmed | Towards the ’Verified Verifier’. Theory and Practice |
| title_short | Towards the ’Verified Verifier’. Theory and Practice |
| title_sort | towards the verified verifier theory and practice |
| topic | верификация спецификация аксиоматическая семантика язык c-light условие корректности метагенерация |
| url | https://www.mais-journal.ru/jour/article/view/72 |
| work_keys_str_mv | AT dakondratyev towardstheverifiedverifiertheoryandpractice AT avpromsky towardstheverifiedverifiertheoryandpractice |