mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic

Abstract

Abstract is an open-source tool for specifying transition systems in first-order logic and reasoning about them. is particularly suitable for analyzing and verifying distributed algorithms. implements key functionalities needed for safety verification and provides flexible interfaces that make it useful not only as a verification tool but also as a research platform for developing verification techniques, and in particular invariant inference algorithms. Moreover, the input language is both simple and general, and the repository includes several dozen benchmarks—transition systems that model a wide range of distributed and concurrent algorithms. has supported several recent research efforts that benefited from its development framework and benchmark set.