From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation

Allan Blanchard
(Univ. Orléans, INSA Centre Val de Loire, France)
Frédéric Loulergue
(Northern Arizona University, School of Informatics Computing and Cyber Systems, Flagstaff, USA)
Nikolai Kosmatov
(Software Reliability Laboratory, CEA LIST, France)

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 Alexei Lisitsa, Andrei P. Nemytykh and Maurizio Proietti: Proceedings Fifth International Workshop on Verification and Program Transformation (VPT 2017), Uppsala, Sweden, 29th April 2017, Electronic Proceedings in Theoretical Computer Science 253, pp. 109–123.
Published: 23rd August 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.253.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org