PV2 Hampasynthesises a replicated object that guarantees integrity, convergence and recency

Application domain/field

Type of tool

Synthesis tool

Internals

Replicas are often used for fault-tolerance, availability, responsiveness and scalability. We need some kind of coordination between replicated objects, e.g. using consensus protocols, to keep all objects up-to-date/synchronised. This tool provides a correct-by-construction replicated object that guarantees (1) integrity, (2) convergence, and (3) recency. This replicated object is automatically synthesized based on a given sequential object with the declaration of its integrity and recency requirements. Uses CVC4.
Synthesis

Links

Artifact: https://github.com/XiaoLi0614/HampaAE

Last commit date

22 April 2020

Related papers

https://doi.org/10.1007/978-3-030-53288-8_16

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.