Synthesis is the process of automatically constructing an implementation from a specification. In parameterized synthesis, we construct a single process such that the distributed system consisting of an arbitratry number of copies of the process satisfies a parameterized specification. In this paper, we present PARTY, a tool for parameterized synthesis from specifications in indexed linear temporal logic. Our approach extends SMT-based bounded synthesis, a flexible method for distributed synthesis, to parameterized specifications. In the current version, PARTY can be used to solve the parameterized synthesis problem for token-ring architectures. The tool can also synthesize monolithic systems, for which we provide a comparison to other state-of-the-art synthesis tools.
Computer Aided Verification (CAV)
2013
2026-07-28