Towards verification of C programs: Axiomatic semantics of the C-kernel language
DOI10.1023/B:PACS.0000004134.24714.E5zbMATH Open1099.68544MaRDI QIDQ557549FDOQ557549
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)
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
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)
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
- Title not available (Why is that?)
- Mechanized semantics for the clight subset of the C language
- Logic for reasoning about bugs in loops over data sequences (IFIL)
Uses Software
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)
