<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>

COPY SCRIPT

For further information contact us at helpdesk@openaire.eu

Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model — proof artifact

integration_instructionsResearch softwarekeyboard_double_arrow_right Software 03 Jul 2021 English Publisher:Zenodo

Authors: Mével, Glen; Jourdan, Jacques-Henri;

doi: 10.5281/zenodo.5064045 , 10.5281/zenodo.5064044

Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model — proof artifact

- Summary
- Related research
  (1)
- Metrics

Abstract

This is the artifact that accompanies the paper “Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model“, published at the ICFP 2021 conference. The artifact consists in a set of Coq proof scripts. A plain source code archive is provided, as well as a virtual machine in which all dependencies are already installed and the project already compiled. This project is developped in this git repository, which also contains the paper.

Related Organizations

French National Centre for Scientific Research
France
University of Paris-Saclay
France
Laboratoire Méthodes Formelles
France

1 Research products, page 1 of 1

Formal verification of a concurrent bounded queue in a weak memory model
descriptionPublication2021IsSupplementTo
linkLink to
shareshareShare
citeCite
addClaim
Please grant OpenAIRE to access and update your ORCID works.
This Research product is the result of merged Research products in OpenAIRE.

You have already added works in your ORCID record related to the merged Research product.
This Research product is the result of merged Research products in OpenAIRE.

You have already added works in your ORCID record related to the merged Research product.
Select content type to embed
All Research products
arrow_drop_down
<script type="text/javascript">  </script>
COPY SCRIPT
For further information contact us at helpdesk@openaire.eu
more_vert
linkLink to
shareshareShare
citeCite
addClaim
Please grant OpenAIRE to access and update your ORCID works.
This Research product is the result of merged Research products in OpenAIRE.

You have already added works in your ORCID record related to the merged Research product.
This Research product is the result of merged Research products in OpenAIRE.

You have already added works in your ORCID record related to the merged Research product.
Select content type to embed
All Research products
arrow_drop_down
<script type="text/javascript">  </script>
COPY SCRIPT
For further information contact us at helpdesk@openaire.eu

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average