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

Application domain/field

• Verification
• Asynchronous fault-tolerant distributed systems

Type of tool

Rewriter/translator

Expected input

• Asynchronous fault-tolerant protocol, e.g. a leader election protocol, in a C embedding of the language specified in the paper
• Configuration file

Format:

Protocol: C embedding of their language. Be aware:

• can only contain C99-like syntactic constructions
• all code has to be in a main() function
• directives and headers are not supported
• if and else tokens are followed by curly braces

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.