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_ | 1826558970079215616 |
|---|---|
| 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 | 2025-03-14T08:52:57Z |
| publishDate | 2014-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-7714fc9a1e834e80aee06df037fb1fe42025-03-02T12:46:56ZengYaroslavl 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 |