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

Last commit date

27 June 2019

Related papers

https://doi.org/10.1007/978-3-030-25543-5_20

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



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