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

Application domain/field

• Replicated objects
• Synthesis

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.