Conference devoted to the 90th anniversary of Alexei A. Lyapunov

Akademgorodok, Novosibirsk, Russia, October 8-11, 2001,
(state registration number 0320300064)

Abstracts

Programmirung

Towards C programs verification. Language C-light.

Nepomniaschy V.A., Anureev I.S., Michailov I.N., Promsky A.V.

IIS (Novosibirsk)

The paper presents the language C-light which is representative ve-ri-fi-cation-oriented subset of standard C. This language allows deterministic expressions and limited use of statements switch and goto. C-light includes C$++$ operators new and delete to manage dynamic memory instead of standard C library functions. The full structural operational semantics of C-light in the style of Plotkin is presented. The use of C-light as an input language of program verification system is intended.

Full Text in Russian: HTML
Note. Abstracts are published in author's edition

Comments

[Home]
[Conference]

©2001, Siberian Branch of Russian Academy of Science, Novosibirsk
©2001, United Institute of Computer Science SB RAS, Novosibirsk
©2001, Institute of Computational Techologies SB RAS, Novosibirsk
©2001, A.P. Ershov Institute of Informatics Systems SB RAS, Novosibirsk
©2001, Institute of Mathematics SB RAS, Novosibirsk
©2001, Institute of Cytology and Genetics SB RAS, Novosibirsk
©2001, Institute of Computational Mathematics and Mathematical Geophysics SB RAS, Novosibirsk
©2001, Novosibirsk State University
Last modified 06-Jul-2012 (11:45:21)