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

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

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 pro...

Full description

Bibliographic Details
Main Authors: Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
Format: Article
Language:English
Published: Open Publishing Association 2017-08-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1708.07226v1
id doaj-1b729d4685514244b1787bbabf696bfc
record_format Article
spelling doaj-1b729d4685514244b1787bbabf696bfc2020-11-25T00:11:29ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-08-01253Proc. VPT 201710912310.4204/EPTCS.253.9:6From Concurrent Programs to Simulating Sequential Programs: Correctness of a TransformationAllan Blanchard0Frédéric Loulergue1Nikolai Kosmatov2 Univ. Orléans, INSA Centre Val de Loire, France Northern Arizona University, School of Informatics Computing and Cyber Systems, Flagstaff, USA 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.http://arxiv.org/pdf/1708.07226v1
collection DOAJ
language English
format Article
sources DOAJ
author Allan Blanchard
Frédéric Loulergue
Nikolai Kosmatov
spellingShingle Allan Blanchard
Frédéric Loulergue
Nikolai Kosmatov
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
Electronic Proceedings in Theoretical Computer Science
author_facet Allan Blanchard
Frédéric Loulergue
Nikolai Kosmatov
author_sort Allan Blanchard
title From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
title_short From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
title_full From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
title_fullStr From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
title_full_unstemmed From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
title_sort from concurrent programs to simulating sequential programs: correctness of a transformation
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2017-08-01
description 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.
url http://arxiv.org/pdf/1708.07226v1
work_keys_str_mv AT allanblanchard fromconcurrentprogramstosimulatingsequentialprogramscorrectnessofatransformation
AT fredericloulergue fromconcurrentprogramstosimulatingsequentialprogramscorrectnessofatransformation
AT nikolaikosmatov fromconcurrentprogramstosimulatingsequentialprogramscorrectnessofatransformation
_version_ 1725403722861772800

Similar Items