# BoSy: An Experimentation Framework for Bounded Synthesis

arXiv: https://arxiv.org/abs/1803.09566 · HTML: https://mlsanity.com/paper/1803.09566/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Mar 2018.

## Built on by (most cited first, 8 of 8)

- [ChipGPT: How far are we from natural language hardware design](https://mlsanity.com/paper/2305.14019/) (2023)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models](https://mlsanity.com/paper/2605.15131/) (2026)

## Abstract (arXiv)

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.