Two-level mixed verification method of C-light programs in terms of safety logic

MaRDI QIDQ2979840zbMATH OpenFDO

Authors Igor S. Anureev, Il'Ya Mar'Yasov, V. A. Nepomnyashchij

Publication date 26 April 2017

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

zbMATH Keywords

structured operational semantics

Mathematics Subject Classification ID

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

• The problems of C program verification
• A three-stage method of C program verification
• Towards verification of C programs. C-light language and its formal semantics
• Towards verification of C programs: Axiomatic semantics of the C-kernel language
• scientific article; zbMATH DE number 2186292

Cited in

(2)

• Towards verification of C programs. C-light language and its formal semantics
• The problems of C program verification

Describes a project that uses

Uses Software

• C-Light
• Boogie
• Dafny
• VCC

This page was built for publication: Two-level mixed verification method of C-light programs in terms of safety logic

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