Region analysis for deductive verification of C programs

DOI10.1134/S0361768816050042MaRDI QIDQ2216720zbMATH OpenFDO

Authors M. U. Mandrykin, A. V. Khoroshilov

Publication date 16 December 2020

Published in Programming and Computer Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1134/S0361768816050042

Mathematics Subject Classification ID

Theory of programming languages (68N15) 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

• Reasoning about memory layouts
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Automating deductive verification for weak-memory programs
• Exploiting pointer analysis in memory models for deductive verification
• Formal verification of C systems code. Structured types, separation logic and theorem proving

Cites work

• A theory of type polymorphism in programming
• An axiomatic basis for computer programming
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• Types and programing languages

Cited in

(4)

• Verifying pointer and string analyses with region type systems
• Exploiting pointer analysis in memory models for deductive verification
• scientific article; zbMATH DE number 1231585 (Why is no real title available?)
• Reasoning about memory layouts

Describes a project that uses

Uses Software

• VCC
• ML
• Frama-C

This page was built for publication: Region analysis for deductive verification of C programs

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