Program
Verification
Book

PV4 ⊧ BoSyproves realisability of a given property

Application domain/field

Reactive synthesis
LTL synthesis
Bounded synthesis

Type of tool

Synthesis tool

Expected input

LTL formula

Format:

JSON based format

Expected output

Whether a specification is realisable. If realisable, then a solution can be extracted.

Internals

Constraint-solving The tool uses bounded synthesis, this means that it results in a minimal implementation.

Comments

BoSyHyper is from the same team but for synthesis of HyperLTL.

Links

Project page: https://www.react.uni-saarland.de/tools/bosy/
Repository: https://github.com/reactive-systems/bosy
- Last commit date: 21 Jul 2022 (default branch)
- Last commit date: 21 Jul 2022 (last activity)
Online interface: https://www.react.uni-saarland.de/tools/online/BoSy/

Related papers

Realizing $ω$ -regular Hyperproperties (CAV '20)
BoSy: An Experimentation Framework for Bounded Synthesis (CAV '17)
Encodings of Bounded Synthesis (TACAS '17)

Last publication date

14 July 2020

ProVerB specific

Markdown description: view/edit
Reason for this entry: CAV 2020
Contained in the ProVerB22 dataset (paper + artefact)

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