The problems of C program verification

zbMATH Open1374.68297MaRDI QIDQ2963876FDOQ2963876

Authors:

Publication date: 21 February 2017

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

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

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)

Cited In (6)

• A three-stage method of C program verification
• Title not available (Why is that?)
• Two-level mixed verification method of C-light programs in terms of safety logic
• The C\#-light project: solutions of some verification challenges
• Towards verification of C programs. C-light language and its formal semantics
• Semi-automated reasoning about non-determinism in C expressions

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)