<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

TLAPS Safety Proof of MongoRaftReconfig

integration_instructionsResearch softwarekeyboard_double_arrow_right Software 23 Sep 2021Publisher:Zenodo

Authors: Schultz, William; Dardik, Ian;

doi: 10.5281/zenodo.5525483 , 10.5281/zenodo.5525484 , 10.5281/zenodo.5768484

TLAPS Safety Proof of MongoRaftReconfig

- Summary
- Related research
  (2)
- Metrics

Abstract

Supplementary materials for formal verification of safety of the MongoRaftReconfig protocol in TLAPS, the TLA+ proof system. Includes a formal inductive invariant and a TLAPS proof of the LeaderCompleteness and StateMachineSafety properties. MongoRaftReconfig is a logless dynamic reconfiguration protocol originally designed for MongoDB, a distributed database that uses a log-based replication protocol derived from Raft.

Related Organizations

Northeastern University
China (People's Republic of)

2 Research products, page 1 of 1

MongoRaftReconfig TLA+ Specifications
integration_instructionsResearch software2021IsAmongTopNSimilarDocuments
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
Design and Analysis of a Logless Dynamic Reconfiguration Protocol
descriptionPublication2021IsAmongTopNSimilarDocuments
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).	1
	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