C-programs verification based on mixed axiomatic semantics

descriptionPublicationkeyboard_double_arrow_right Article 01 Dec 2011 English Publisher:Allerton PressJournal:Automatic Control and Computer Sciences, volume 45, pages 485-500 (issn: 0146-4116, eissn: 1558-108X,

Copyright policy )

Authors: Igor S. Anureev; Ilya V. Maryasov; Valery A. Nepomniaschy;

doi: 10.3103/s0146411611070029

C-programs verification based on mixed axiomatic semantics

- Summary
- Related research
  (11)
- Metrics

Abstract

The mixed axiomatic semantics of the C-kernel language is described. This language is the kernel of a representative subset which is called C-light. Such semantics makes possible for the verification conditions to be simplified in many cases. The semantics is the basis of the verification conditions generator for C-kernel programs. An example illustrating the application of the inference rules of the semantics is considered.

Related Organizations

A.P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences
Russian Federation
Siberian Branch of the Russian Academy of Sciences
Russian Federation
Russian Academy of Sciences
Russian Federation

11 Research products, page 1 of 2

Loop Invariants Elimination for Definite Iterations over Unchangeable Data Structures in C Programs
2016IsAmongTopNSimilarDocuments
???? ???????? ?? ?????????????????????? ??-????????????????. ???????? c-light ?? ?????? ?????????????????????????????????? ??????????????????
2008IsAmongTopNSimilarDocuments
C Program Verification: VC Explanation and the Standard Library
2011IsAmongTopNSimilarDocuments
MOESM2 of An alternative covariance estimator to investigate genetic heterogeneity in populations
2015IsAmongTopNSimilarDocuments
Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System
2021IsAmongTopNSimilarDocuments
Implementing the Symbolic Method of Verification in the C-Light Project
2018IsAmongTopNSimilarDocuments
Attribute annotations and their use in C program deductive verification
2012IsAmongTopNSimilarDocuments
C program verification: Verification condition explanation and standard library
2012IsAmongTopNSimilarDocuments
Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language
2003IsAmongTopNSimilarDocuments
Automatic C Program Verification Based on Mixed Axiomatic Semantics
2014IsAmongTopNSimilarDocuments

chevron_left
1
2
chevron_right

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	7
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Top 10%
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average