PV2 ATHOS: Asynchronous to HO Synchronizercomputes the synchronous counterpart of an asynchronous protocol

Application domain/field

Type of tool

Rewriter/translator

Expected input

Format:

Protocol: C embedding of their language. Be aware: Configuration file: .py file

Expected output

Round-based synchronous protocol (C file) that is the counterpart of the input (the asynchronous version)

Internals

Uses Verifast

Comments

Reduces the verification of asynchronous fault-tolerant protocols to the verification of round-based synchronous protocols. The Github repository contains examples of configuration files and protocols.
C Protocol

Links

https://github.com/alexandrumc/async-to-sync-translation

Related papers

Communication-Closed Asynchronous Protocols

Last publication date

12 July 2019

ProVerB specific



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