From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
Allan Blanchard (Univ. Orl\'eans, INSA Centre Val de Loire, France),, Fr\'ed\'eric Loulergue (Northern Arizona University, School of Informatics, Computing, Cyber Systems, Flagstaff, USA), Nikolai Kosmatov (Software, Reliability Laboratory, CEA LIST, France)
TL;DR
This paper formalizes and proves the correctness of a program transformation that converts concurrent C programs into sequential ones, enabling existing analysis tools to handle concurrency effectively.
Contribution
It introduces Conc2Seq, a Frama-C plugin that transforms concurrent programs into sequential ones, with formal correctness proofs and mechanization using Coq.
Findings
Formal correctness of the transformation is established.
Proofs are mechanized in Coq for increased reliability.
The approach enables existing tools to analyze concurrent C programs.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.