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., 2010, Volume 17, Number 4, Pages 88–100 (Mi mais39)  

This article is cited in 6 scientific papers (total in 6 papers)

C program verification in the multilanguage system spectrum

V. A. Nepomnyashchiiab, I. S. Anureeva, M. M. Atuchinb, I. V. Mar'yasova, A. A. Petrovb, A. V. Promskiia

a A. P. Ershov Institute of Informatics Systems Sib. Br. RAS
b Novosibirsk State University

Abstract: This paper presents the expendable multi-language analysis and verification system SPECTRUM, which is being developed within the framework of the project SPECTRUM. The project prospects are discussed using the example of C program verification. The project aims at the development of a new integrated approach to program verification which will allow the integration, unification and combination of program verification techniques together with accumulation and reuse of knowledge about them. One of the project features consists in the use of the specialized executable specification language Atoment. This language provides a unified format to represent both verification methods and data for them (program models, annotations, logic formulas). The C-targeted component of the SPECTRUM system is based on our two-level C program verification method. This method represents a good illustration of the integrated approach, since it provides a complex C program verification that combines operational, axiomatic and transformational approaches.

Keywords: verification, specification, operational semantics, axiomatic semantics, domain-specific languages, verification systems

Full text: PDF file (293 kB)
References: PDF file   HTML file
UDC: 519.681
Received: 18.10.2010

Citation: V. A. Nepomnyashchii, I. S. Anureev, M. M. Atuchin, I. V. Mar'yasov, A. A. Petrov, A. V. Promskii, “C program verification in the multilanguage system spectrum”, Model. Anal. Inform. Sist., 17:4 (2010), 88–100

Citation in format AMSBIB
\Bibitem{NepAnuAtu10}
\by V.~A.~Nepomnyashchii, I.~S.~Anureev, M.~M.~Atuchin, I.~V.~Mar'yasov, A.~A.~Petrov, A.~V.~Promskii
\paper C program verification in the multilanguage system spectrum
\jour Model. Anal. Inform. Sist.
\yr 2010
\vol 17
\issue 4
\pages 88--100
\mathnet{http://mi.mathnet.ru/mais39}


Linking options:
  • http://mi.mathnet.ru/eng/mais39
  • http://mi.mathnet.ru/eng/mais/v17/i4/p88

    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

    This publication is cited in the following articles:
    1. M. M. Atuchin, I. S. Anureev, “Atributnye annotatsii i ikh primenenie v deduktivnoi verifikatsii C-programm”, Model. i analiz inform. sistem, 18:4 (2011), 21–33  mathnet
    2. I. S. Anureev, “Tipovye primery ispolzovaniya yazyka Atoment”, Model. i analiz inform. sistem, 18:4 (2011), 7–20  mathnet
    3. I. S. Anureev, “Deduktivnaya verifikatsiya telekommunikatsionnykh sistem, predstavlennykh na yazyke Si”, Model. i analiz inform. sistem, 19:6 (2012), 34–44  mathnet
    4. I. S. Anureev, “Na puti k tekhnologii razrabotki operatsionnoi semantiki kompyuternykh yazykov: unifitsirovannyi format pomechennykh sistem perekhodov”, Tr. SPIIRAN, 25 (2013), 255–276  mathnet
    5. I. S. Anureev, S. N. Baranov, D. M. Beloglazov, E. V. Bodin, P. D. Drobintsev, A. V. Kolchin, V. P. Kotlyarov, A. A. Letichevskii, A. A. Letichevskii, V. A. Nepomnyaschii, I. V. Nikiforov, S. V. Potienko, L. V. Priima, B. V. Tyutin, “Sredstva podderzhki integrirovannoi tekhnologii dlya analiza i verifikatsii spetsifikatsii telekommunikatsionnykh prilozhenii”, Tr. SPIIRAN, 26 (2013), 349–383  mathnet
    6. M. S. Ushakova, A. I. Legalov, “Instrumentalnaya podderzhka formalnoi verifikatsii programm, napisannykh na yazyke funktsionalno-potokovogo parallelnogo programmirovaniya”, Vestn. YuUrGU. Ser. Vych. matem. inform., 4:2 (2015), 58–70  mathnet  crossref  elib
  • Моделирование и анализ информационных систем
    Number of views:
    This page:237
    Full text:86
    References:31

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