The problems of C program verification

MaRDI QIDQ2963876zbMATH OpenFDO

Authors

Publication date 21 February 2017

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

zbMATH Keywords

automatic verificationC-kernel languagetranslation ruleverification condition

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A three-stage method of C program verification
• The C\#-light project: solutions of some verification challenges
• Towards verification of C programs. C-light language and its formal semantics
• Two-level mixed verification method of C-light programs in terms of safety logic
• scientific article; zbMATH DE number 1377354

Cited in

(6)

• The C\#-light project: solutions of some verification challenges
• Semi-automated reasoning about non-determinism in C expressions
• scientific article; zbMATH DE number 2186292 (Why is no real title available?)
• A three-stage method of C program verification
• 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

Describes a project that uses

Uses Software

• z3
• SIMPLIFY
• C-Light

This page was built for publication: The problems of C program verification

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