PV2 FACTEST: Fast Controller Synthesis frameworksynthesises a controller for non-linear systems with reach-avoid requirements

Application domain/field

Type of tool

Synthesis tool

Expected input


Python, it expects certain function names, and return values.

Expected output

A reference trajectory and reference input for every partition (or none if it could not be found)


FACTEST synthesizes a controller for non-linear systems with reach-avoid requirements. Non-linear systems/vehicles are vehicles such as cards, drones, and underwater vehicles. The reach-avoid requirement states that a certain goal set should be reached while avoiding any obstacles in the trajectory. Uses Pypoman, Yices, SciPy, NumPy


Note, the paper that introduced RealSyn is mentioned as previous work on the project page.


Related papers

Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models

Last publication date

14 July 2020

ProVerB specific

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