AbsSynthe: abstract synthesis from succinct safety specifications

AbsSynthe: abstract synthesis from succinct safety specifications

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 organizer...

Full description

Bibliographic Details
Main Authors: Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, Ocan Sankur
Format: Article
Language:English
Published: Open Publishing Association 2014-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1407.5961v1
id doaj-41354c88bce04256a7ecf4fcbc745331
record_format Article
spelling doaj-41354c88bce04256a7ecf4fcbc7453312020-11-24T22:54:37ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-07-01157Proc. SYNT 201410011610.4204/EPTCS.157.11:4AbsSynthe: abstract synthesis from succinct safety specificationsRomain Brenguier0Guillermo A. Pérez1Jean-François Raskin2Ocan Sankur3 Université Libre de Bruxelles Université Libre de Bruxelles Université Libre de Bruxelles Université Libre de Bruxelles 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.http://arxiv.org/pdf/1407.5961v1
collection DOAJ
language English
format Article
sources DOAJ
author Romain Brenguier
Guillermo A. Pérez
Jean-François Raskin
Ocan Sankur
spellingShingle Romain Brenguier
Guillermo A. Pérez
Jean-François Raskin
Ocan Sankur
AbsSynthe: abstract synthesis from succinct safety specifications
Electronic Proceedings in Theoretical Computer Science
author_facet Romain Brenguier
Guillermo A. Pérez
Jean-François Raskin
Ocan Sankur
author_sort Romain Brenguier
title AbsSynthe: abstract synthesis from succinct safety specifications
title_short AbsSynthe: abstract synthesis from succinct safety specifications
title_full AbsSynthe: abstract synthesis from succinct safety specifications
title_fullStr AbsSynthe: abstract synthesis from succinct safety specifications
title_full_unstemmed AbsSynthe: abstract synthesis from succinct safety specifications
title_sort abssynthe: abstract synthesis from succinct safety specifications
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2014-07-01
description 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.
url http://arxiv.org/pdf/1407.5961v1
work_keys_str_mv AT romainbrenguier abssyntheabstractsynthesisfromsuccinctsafetyspecifications
AT guillermoaperez abssyntheabstractsynthesisfromsuccinctsafetyspecifications
AT jeanfrancoisraskin abssyntheabstractsynthesisfromsuccinctsafetyspecifications
AT ocansankur abssyntheabstractsynthesisfromsuccinctsafetyspecifications
_version_ 1725658768834822144

Similar Items