Automatic C program verification based on mixed axiomatic semantics | Zendy

I. V. Maryasov | Zendy; V. A. Nepomnyaschy | Zendy; A. V. Promsky | Zendy; Dmitry Kondratyev | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Automatic C program verification based on mixed axiomatic semantics

Author(s) -

I. V. Maryasov,

V. A. Nepomnyaschy,

A. V. Promsky,

Dmitry Kondratyev

Publication year - 2014

Publication title -

automatic control and computer sciences

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.299

H-Index - 17

eISSN - 1558-108X

pISSN - 0146-4116

DOI - 10.3103/s0146411614070141

Subject(s) - computer science , programming language , rotation formalisms in three dimensions , semantics (computer science) , implementation , axiom , operational semantics , axiomatic semantics , theoretical computer science , denotational semantics , geometry , mathematics

The development of the C-light project led to the application of new formalisms and method implementations that facilitate the verification of C programs. The mixed axiomatic semantics provides a choice between simplified and general inference rules of verification conditions (VC) depending on the program objects and their properties. The LLVM infrastructure greatly simplifies the implementation of the analyzer and translator of C-light programs. The semantic labeling method proposed earlier can now be safely used in verification conditions during their proving. A program from well-known verification competition is considered in order to illustrate the applicability of the system.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research