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

Application domain/field

Type of tool

Synthesis tool


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.


Related papers

Hampa: Solver-Aided Recency-Aware Replication

Last publication date

14 July 2020

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.