PV2 PARTYgenerates an automaton from source code or spec

Bounded synthesis tool that supports CTL* synthesis

Application domain/field

Type of tool

Synthesis tool

Expected input

Specification file


Expected output

If realisable, then an automaton in dot or AIGER format.


Automaton LTL Synthesis


Repository: https://github.com/5nizza/party-elli

Related papers

Last publication date

13 July 2017

ProVerB specific

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