Automated domain-specific C verification with mbeddr

Zaur Molotnikov, Markus Völter, Daniel Ratiu

Abstract

When verifying C code, two major problems must be addressed. One is the specification of the verified systems properties, the other one is the construction of the verification environment. Neither C itself, nor existing C verification tools, offer the means to efficiently specify application domain-level properties and environments for verification. These two shortcomings hamper the usability of C verification, and limit its adoption in practice. In this paper we introduce an approach that addresses both problems and results in user-friendly and practically usable C verification. The novelty of the approach is the combination of domain-specific language engineering and C verification. We apply the approach in the domain of state-based software, using mbeddr and CBMC. We validate the implementation with an example from the Pacemaker Challenge, developing a functionally verified, lightweight, and deployable cardiac pulse generator. The approach itself is domain-independent.

BibTeX

@inproceedings{Molotnikov-al:ASE14,
  author    = {Zaur Molotnikov and
               Markus V{\"{o}}lter and
               Daniel Ratiu},
  title     = {Automated domain-specific C verification with mbeddr},
  booktitle = {ASE},
  pages     = {539--550},
  publisher = {{ACM}},
  year      = {2014},
}

Automated domain-specific C verification with mbeddr

Abstract

Related papers