Error-tracing axiomatic semantics for C-kernel

MaRDI QIDQ2979813zbMATH OpenFDO

Authors

Publication date 26 April 2017

Full work available at URL http://bulletin.iis.nsk.su/files/article/promsky_0.pdf

zbMATH Keywords

extended Hoare logicextended Hoare rulesrenderingrewriting

Mathematics Subject Classification ID

Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Towards verification of C programs: Axiomatic semantics of the C-kernel language
• Generating error traces from verification-condition counterexamples
• Explaining Verification Conditions
• Verification conditions for source-level imperative programs
• TRACER: a symbolic execution tool for verification

Cited in

(4)

• Generating error traces from verification-condition counterexamples
• scientific article; zbMATH DE number 1555194 (Why is no real title available?)
• Explaining Verification Conditions
• Towards verification of C programs: Axiomatic semantics of the C-kernel language

Describes a project that uses

Uses Software

• VCC
• C-Light

This page was built for publication: Error-tracing axiomatic semantics for C-kernel

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