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...
Saved in:
| 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 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849240806973505536 |
|---|---|
| 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. |
| format | Article |
| id | doaj-art-7714fc9a1e834e80aee06df037fb1fe4 |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2014-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-7714fc9a1e834e80aee06df037fb1fe42025-08-20T04:00:26ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172014-12-01216718210.18255/1818-1015-2014-6-71-8266Towards the ’Verified Verifier’. Theory and PracticeD. A. Kondratyev0A. V. Promsky1Novosibirsk State UniversityA.P. Ershov Institute of Informatics Systems SB RASAs 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/72verificationspecificationaxiomatic semanticsthe c-light languageverification conditionmetavcg |
| spellingShingle | D. A. Kondratyev A. V. Promsky Towards the ’Verified Verifier’. Theory and Practice Моделирование и анализ информационных систем verification specification axiomatic semantics the c-light language verification condition metavcg |
| 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 | verification specification axiomatic semantics the c-light language verification condition metavcg |
| url | https://www.mais-journal.ru/jour/article/view/72 |
| work_keys_str_mv | AT dakondratyev towardstheverifiedverifiertheoryandpractice AT avpromsky towardstheverifiedverifiertheoryandpractice |