|
Modelirovanie i Analiz Informatsionnykh Sistem, 2010, Volume 17, Number 3, Pages 5–28
(Mi mais20)
|
|
|
|
This article is cited in 5 scientific papers (total in 5 papers)
C-programs verification on basis of mixed axiomatic semantics
I. S. Anureev, I. V. Mar'yasov, V. A. Nepomnyashchii A. P. Ershov Institute of Informatics Systems Sib. Br. RAS
Abstract:
The mixed axiomatic semantics of a C-kernel language is described. This language is the kernel of a representative C language subset which is called C-light. Such semantics allows to simplify the verification conditions in many cases. This semantics is a base of verification conditions generator of C-kernel programs. An example which illustrates the use of inference rules of the semantics is considered.
Keywords:
program verification, operational semantics, axiomatic semantics, C language, C-light language, C-kernel language, partial correctness.
Received: 25.05.2010
Citation:
I. S. Anureev, I. V. Mar'yasov, V. A. Nepomnyashchii, “C-programs verification on basis of mixed axiomatic semantics”, Model. Anal. Inform. Sist., 17:3 (2010), 5–28
Linking options:
https://www.mathnet.ru/eng/mais20 https://www.mathnet.ru/eng/mais/v17/i3/p5
|
Statistics & downloads: |
Abstract page: | 475 | Full-text PDF : | 150 | References: | 54 |
|