AbsSynthe: abstract synthesis from succinct safety specifications
Romain Brenguier (Universit\'e Libre de Bruxelles), Guillermo A., P\'erez (Universit\'e Libre de Bruxelles), Jean-Fran\c{c}ois Raskin, (Universit\'e Libre de Bruxelles), Ocan Sankur (Universit\'e Libre de, Bruxelles)
TL;DR
AbsSynthe introduces a synthesis algorithm for safety specifications in circuit form, utilizing fixpoint computations, abstraction, and BDDs, with evaluation on synthesis competition benchmarks.
Contribution
The paper presents a novel synthesis method combining fixpoint, abstraction, and BDDs for safety specifications, demonstrated on standard benchmarks.
Findings
Effective synthesis on SYNT'14 benchmarks
Utilizes fixpoint, abstraction, and BDDs for safety circuit synthesis
Achieves promising results in safety specification synthesis
Abstract
In this paper, we describe a synthesis algorithm for safety specifications described as circuits. Our algorithm is based on fixpoint computations, abstraction and refinement, it uses binary decision diagrams as symbolic data structure. We evaluate our tool on the benchmarks provided by the organizers of the synthesis competition organized within the SYNT'14 workshop.
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.