Abstract

Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed Conc2Seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs.

In this paper we formalize and sketch the proof of correctness of the program transformation principle behind Conc2Seq, and present an effort towards the full mechanization of both the formalization and proofs with the proof assistant Coq.

In

Proc. of the 5th International Workshop on Verification and Program Transformation (VPT 2017)

ETAPS 2017 Workshops, Uppsala, Sweden, April 2017, EPTCS, vol. 253, pages 109-123.

Final publication available at DOI: 10.4204/EPTCS.253.9.

Paper (Available PDF is the author's final version of the work)

Slides