BoSy: An Experimentation Framework for Bounded Synthesis
Peter Faymonville, Bernd Finkbeiner, Leander Tentrup

TL;DR
BoSy is a versatile framework for reactive synthesis using bounded synthesis, encoding solutions into various logical formalisms, and supporting solution extraction and verification, with applications in experimentation and solver evaluation.
Contribution
Introduces BoSy, a flexible bounded synthesis framework that integrates multiple solver types and supports solution extraction and verification, advancing synthesis experimentation.
Findings
BoSy successfully synthesized reactive systems with minimal size.
It encodes synthesis problems into SAT, QBF, DQBF, EPR, and SMT.
BoSy won the LTL synthesis track at SYNTCOMP 2016.
Abstract
We present BoSy, a reactive synthesis tool based on the bounded synthesis approach. Bounded synthesis ensures the minimality of the synthesized implementation by incrementally increasing a bound on the size of the solutions it considers. For each bound, the existence of a solution is encoded as a logical constraint solving problem that is solved by an appropriate solver. BoSy constructs bounded synthesis encodings into SAT, QBF, DQBF, EPR, and SMT, and interfaces to solvers of the corresponding type. When supported by the solver, BoSy extracts solutions as circuits, which can, if desired, be verified with standard hardware model checkers. BoSy won the LTL synthesis track at SYNTCOMP 2016. In addition to its use as a synthesis tool, BoSy can also be used as an experimentation and performance evaluation framework for various types of satisfiability solvers.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Software Reliability and Analysis Research
