RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Model. Anal. Inform. Sist.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Model. Anal. Inform. Sist., 2014, Volume 21, Number 6, Pages 71–82 (Mi mais413)  

Towards the verified verifier. Theory and practice

D. A. Kondratyeva, A. V. Promskyb

a Novosibirsk State University, ul. Pirogova, 2, Novosibirsk, 630090, Russia
b A. P. Ershov Institute of Informatics Systems SB RAS, Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia

Abstract: 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.

Keywords: verification, specification, axiomatic semantics, the C-light language, verification condition, MetaVCG.

Full text: PDF file (504 kB)
References: PDF file   HTML file
UDC: 519.681
Received: 13.09.2014

Citation: D. A. Kondratyev, A. V. Promsky, “Towards the verified verifier. Theory and practice”, Model. Anal. Inform. Sist., 21:6 (2014), 71–82

Citation in format AMSBIB
\Bibitem{KonPro14}
\by D.~A.~Kondratyev, A.~V.~Promsky
\paper Towards the verified verifier. Theory and practice
\jour Model. Anal. Inform. Sist.
\yr 2014
\vol 21
\issue 6
\pages 71--82
\mathnet{http://mi.mathnet.ru/mais413}


Linking options:
  • http://mi.mathnet.ru/eng/mais413
  • http://mi.mathnet.ru/eng/mais/v21/i6/p71

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Number of views:
    This page:94
    Full text:33
    References:15

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2020