Towards verification of C programs: Axiomatic semantics of the C-kernel language

DOI10.1023/B:PACS.0000004134.24714.E5MaRDI QIDQ557549zbMATH OpenFDO

Authors V. A. Nepomniaschy, Igor S. Anureev, A. V. Promskii

Publication date 30 June 2005

Published in Programming and Computer Software (Search for Journal in Brave)

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Towards verification of C programs. C-light language and its formal semantics
• Error-tracing axiomatic semantics for C-kernel
• Towards verification of C\(\#\) programs: a three-level approach
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• scientific article; zbMATH DE number 2186292

Cited in

(10)

• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Towards verification of C\(\#\) programs: a three-level approach
• Two-level mixed verification method of C-light programs in terms of safety logic
• Towards verification of C programs. C-light language and its formal semantics
• Error-tracing axiomatic semantics for C-kernel
• An operational and axiomatic semantics for non-determinism and sequence points in C
• Operational ontological approach to formal programming language specification
• scientific article; zbMATH DE number 3926271 (Why is no real title available?)
• Mechanized semantics for the clight subset of the C language
• Logic for reasoning about bugs in loops over data sequences (IFIL)

Describes a project that uses

Uses Software

• C-Light

This page was built for publication: Towards verification of C programs: Axiomatic semantics of the C-kernel language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q557549)