Skip to main content
SpringerLink
Log in

Implementing the Symbolic Method of Verification in the C-Light Project

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10742))

Abstract

The C-light is a project aimed onto deductive verification of C programs. It relies on three basic ideas, namely—metageneration of verification conditions (MetaVCG), semantic mark-up and the symbolic method, two-level verification that uses C-light language as a front-end and C-kernel language as a back-end. The semantic mark-up extends the standard Hoare inference rules by semantic labels for explanations of failed verification conditions. The symbolic method is based on a replacement of each for-loop by a single assignment with a cumulative effect, it allows us to avoid explicit invariant generation. However, to make verification efficient, it is necessary to develop new techniques instead of the replacement. These new techniques for verification of linear algebra programs is presented and explained in this article.

This research was in part supported by RFBR (grant No. 15-01-05974 and grant No. 17-01-00789).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of sequential and concurrent programs, p. 450. Springer, London (1991). https://doi.org/10.1007/978-1-84882-745-5

    Book  MATH  Google Scholar 

  2. Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_2

    Chapter  Google Scholar 

  3. Denney, E., Fischer, B.: Explaining verification conditions. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 145–159. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79980-1_12

    Chapter  Google Scholar 

  4. Filliâtre, J.-C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30482-1_10

    Chapter  Google Scholar 

  5. Fraer, R.: Tracing the origins of verification conditions. In: Wirsing, M., Nivat, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 241–255. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0014320

    Chapter  Google Scholar 

  6. Kondratyev D.A.: The extension of the MetaVCG approach by semantic mark-up concept. In: Proceedings of the International Workshop Conferences on Tools & Methods of Program Analysis, St. Petersburg, pp. 107–118 (2015). (in Russian)

    Google Scholar 

  7. Leino, K.R.M., Millstein, T., Saxe, J.B.: Generating error traces from verification condition counterexamples. Sci. Comput. Program. 55(1–3), 209–226 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  8. Maryasov, I.V., Nepomniaschy, V.A.: Loop invariants elimination for definite iterations over unchangeable data structures in C programs. Model. Anal. Inf. Syst. 22(6), 773–782 (2015)

    Article  MathSciNet  Google Scholar 

  9. Moriconi, M., Schwartz, R.L.: Automatic construction of verification condition generators from Hoare logics. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 363–377. Springer, Heidelberg (1981). https://doi.org/10.1007/3-540-10843-2_30

    Chapter  Google Scholar 

  10. Nepomniaschy, V.A.: Symbolic method of verification of definite iterations over altered data structures. Program. Comput. Softw. 31(1), 1–9 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  11. Nepomniaschy, V.A., Anureev, I.S., Promsky, A.V.: Towards verification of C programs: axiomatic semantics of the C-kernel languages. Program. Comput. Softw. 29(6), 338–350 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  12. Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., Promsky, A.V.: Towards verification of C programs. C-light language and its formal semantics. Program. Comput. Softw. 28(6), 314–323 (2002)

    Article  Google Scholar 

  13. Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., Promsky, A.V.: Verification-oriented language C-light. In: System Informatics: Scientific Transactions/RAS. Siberian branch. Institute of Informatics Systems, vol. 9, pp. 51–134 (2004)

    Google Scholar 

  14. Nepomniaschy, V.A., Ryakin, O.M.: Applied methods of program verification. In: Radio and Communication, 256 p. Moscow (1988). (in Russian)

    Google Scholar 

  15. Nepomniaschy, V.A., Sulimov, A.A.: Problem-oriented verification system and its application to linear algebra programs. Theor. Comput. Sci. 119(1), 173–185 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  16. Nepomniaschy, V.A., Sulimov, A.A.: Verification of the linear algebra programs in the system SPECTRUM. Cybern. Syst. Anal. 28(5), 766–774 (1992)

    Article  MATH  Google Scholar 

  17. Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics Systems SB RAS, Novosibirsk, 630090, Russia

    Dmitry Kondratyev

Authors
  1. Dmitry Kondratyev
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dmitry Kondratyev .

Editor information

Editors and Affiliations

  1. Ivannikov Institute for System Programming of RAS, Moscow, Russia

    Alexander K. Petrenko

  2. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kondratyev, D. (2018). Implementing the Symbolic Method of Verification in the C-Light Project. In: Petrenko, A., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2017. Lecture Notes in Computer Science(), vol 10742. Springer, Cham. https://doi.org/10.1007/978-3-319-74313-4_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-74313-4_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-74312-7

  • Online ISBN: 978-3-319-74313-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation