Skip to main content
SpringerLink
Log in

Verification-Oriented Language C-Light and Its Structural Operational Semantics

  • Conference paper
Perspectives of System Informatics (PSI 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2890))

Abstract

The paper presents the language C-light which is a representative verification-oriented subset of the standard C. This language allows deterministic expressions and a limited use of the statements switchand goto. C-light includes the C++ operators newand deleteto manage the dynamic memory instead of standard C library functions. The structural operational semantics of C-light in the Plotkin style is outlined.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Apt, K.R., Olderog, E.R.: Verification of sequential and concurrent programs. Springer, Berlin (1991)

    MATH  Google Scholar 

  2. Gurevich, Y., Huggins, J.K.: The semantics of the C programming language. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 274–309. Springer, Heidelberg (1993)

    Google Scholar 

  3. Huggins, J.K., Shen, W.: The static and dynamic semantics of C (extended abstract). In: Local Proc. Int. Workshop on Abstract State Machines, Zurich, pp. 272–284 (2000) (ETH TIK-Rep.; N 87)

    Google Scholar 

  4. ISO/IEC 9899:1999, Programming languages — C (1999)

    Google Scholar 

  5. Nepomniaschy, V.A., Anureev, I.S., Michailov, I.N., Promsky, A.V.: Towards C program verificaton. The language C-light and its formal semantics. — Programmirovanie (6), 1–13 (2002) (in Russian)

    Google Scholar 

  6. Nepomniaschy, V.A., Anureev, I.S., Michailov, I.N., Promsky, A.V.: Towards C program verificaton. Part 1. Language C-light. — A.P. Ershov Institute of Informatics Systems, Report N 84. — Novosibirsk (2001) (in Russian)

    Google Scholar 

  7. Nepomniaschy, V.A., Anureev, I.S., Michailov, I.N., Promsky, A.V.: Towards C program verificaton. Part 2. Language C-light-kernel and its axiomatic semantics. — A.P. Ershov Institute of Informatics Systems, Report N 87. — Novosibirsk (2001) (in Russian)

    Google Scholar 

  8. Nepomniaschy, V.A., Anureev, I.S., Michailov, I.N., Promsky, A.V.: Towards C program verificaton. Part 3. Translation from C-light into C-light-kernel and its formal justification. A.P. Ershov Institute of Informatics Systems, Report N 97. — Novosibirsk (2002) (in Russian)

    Google Scholar 

  9. Norrish, M.: Deterministic expressions in C. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 147–161. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Norrish, M.: C formalised in HOL.— PhD thesis, Computer Lab., Univ of Cambridge (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Siberian Division of the Russian Academy of Sciences, A. P. Ershov Institute of Informatics Systems, 6, Lavrentiev ave., Novosibirsk, 630090, Russia

    Valery A. Nepomniaschy, Igor S. Anureev & Alexey V. Promsky

Authors
  1. Valery A. Nepomniaschy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Igor S. Anureev
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexey V. Promsky
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technische Universität München, Germany

    Manfred Broy

  2. A.P. Ershov Institute of Informatics Systems, Siberian Branch of Russian Academy of Sciences, 630090, Novosibirsk, Russia

    Alexandre V. Zamulin

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nepomniaschy, V.A., Anureev, I.S., Promsky, A.V. (2004). Verification-Oriented Language C-Light and Its Structural Operational Semantics. In: Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 2003. Lecture Notes in Computer Science, vol 2890. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39866-0_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-39866-0_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20813-6

  • Online ISBN: 978-3-540-39866-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation