reposiTUm: Reactive Synthesis Modulo Theories using Abstraction Refinement

<!DOCTYPE html> <html lang="en"> <head> <title>reposiTUm: Reactive Synthesis Modulo Theories using Abstraction Refinement</title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/> <meta http-equiv="X-UA-Compatible" content="IE=edge"/> <meta name="Generator" content="DSpace CRIS-5.10.0-SNAPSHOT"/> <meta name="viewport" content="width=device-width, initial-scale=1.0"> <link rel="resourcesync sitemap" href="https://repositum.tuwien.at/rs/resourcesync.xml" type="application/xml"/> <link rel="shortcut icon" href="/favicon.ico" type="image/x-icon"/> <link rel="stylesheet" href="/static/comp/css/defaultStyles.min.css"> <link rel="search" type="application/opensearchdescription+xml" href="/open-search/description.xml" title="reposiTUm"/> <link rel="schema.DCTERMS" href="http://purl.org/dc/terms/" /> <link rel="schema.DC" href="http://purl.org/dc/elements/1.1/" /> <meta name="DC.creator" content="Maderbacher, Benedikt" /> <meta name="DC.creator" content="Bloem, Roderick" /> <meta name="DCTERMS.dateAccepted" content="2022-10-13T09:49:03Z" scheme="DCTERMS.W3CDTF" /> <meta name="DCTERMS.available" content="2022-10-13T09:49:03Z" scheme="DCTERMS.W3CDTF" /> <meta name="DCTERMS.issued" content="2022-10" scheme="DCTERMS.W3CDTF" /> <meta name="DCTERMS.bibliographicCitation" content="<div class="csl-bib-body">
 <div class="csl-entry">Maderbacher, B., &#38; Bloem, R. (2022). Reactive Synthesis Modulo Theories using Abstraction Refinement. In A. Griggio &#38; N. Rungta (Eds.), <i>Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022</i> (pp. 315–324). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_38</div>
</div>" /> <meta name="DC.identifier" content="http://hdl.handle.net/20.500.12708/81367" scheme="DCTERMS.URI" /> <meta name="DC.identifier" content="https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_38" scheme="DCTERMS.URI" /> <meta name="DC.language" content="en" scheme="DCTERMS.RFC1766" /> <meta name="DC.rights" content="http://creativecommons.org/licenses/by/4.0/" scheme="DCTERMS.URI" /> <meta name="DC.subject" content="formale Methode" xml:lang="de" /> <meta name="DC.subject" content="formal methods" xml:lang="en" /> <meta name="DC.title" content="Reactive Synthesis Modulo Theories using Abstraction Refinement" xml:lang="en" /> <meta name="DC.type" content="Inproceedings" xml:lang="en" /> <meta name="DC.type" content="Konferenzbeitrag" xml:lang="de" /> <meta name="DC.publisher" content="TU Wien Academic Press" /> <meta name="citation_keywords" content="formale Methode; formal methods; Inproceedings; Konferenzbeitrag" /> <meta name="citation_firstpage" content="315" /> <meta name="citation_title" content="Reactive Synthesis Modulo Theories using Abstraction Refinement" /> <meta name="citation_doi" content="10.34727/2022/isbn.978-3-85448-053-2_38" /> <meta name="citation_language" content="en" /> <meta name="citation_author" content="Maderbacher, Benedikt" /> <meta name="citation_author" content="Bloem, Roderick" /> <meta name="citation_conference" content="#PLACEHOLDER_PARENT_METADATA_VALUE#" /> <meta name="citation_pdf_url" content="https://repositum.tuwien.at/bitstream/20.500.12708/81367/1/Maderbacher-2022-Reactive%20Synthesis%20Modulo%20Theories%20using%20Abstraction%20Ref...-vor.pdf" /> <meta name="citation_abstract_html_url" content="https://repositum.tuwien.at/handle/20.500.12708/81367" /> <meta name="citation_lastpage" content="324" /> <script type='text/javascript' src="/static/comp/js/layout-default.min.js"></script> <script type='text/javascript'> var j = jQuery.noConflict(); var $ = jQuery.noConflict(); var JQ = j; dspaceContextPath = ""; jQuery(document).ready(function ($) { $('span[data-toggle="tooltip"]').tooltip(); $('i[data-toggle="tooltip"]').tooltip(); }); </script> <script type="text/javascript"></script> </head> <body id="body"> <header> <input type="hidden" id="currentLanguageInput" value="en"/> <div id="logo-fixed"> <a class="navbar-brand" href="https://tuwien.at"> <img src="/image/TU-logo.png" class="img-responsive" style="max-height:8vh;"> </a> </div> <nav class="navbar navbar-fixed-top"> <div class="container-fluid"> <div class="navbar-header"> <button type="button" class="navbar-toggle collapsed" data-toggle="collapse" data-target="#navbar" aria-expanded="false" aria-controls="navbar"> <span class="sr-only">Toggle navigation</span> <span class="icon-bar"></span> <span class="icon-bar"></span> <span class="icon-bar"></span> </button> <a id="homeLink" class="navbar-brand" href="/">reposiTUm</a> <button id="languageToggle" type="button" class="btn btn-sm btn-toggle active" data-toggle="button" aria-pressed="false" autocomplete="off" onclick="changeLanguage(this)" data-toggle="tooltip" title="Switch to German"> <div class="handle"></div> </button> </div> <div id="navbar" class="navbar-collapse collapse"> <ul class="nav navbar-nav navbar-right" id="headerLinkList"> <li> <form id="searchprocessor" name="searchprocessor" action="/simple-search" method="get"> <input type="text" class="form-control" id="searchquery" name="query" placeholder="Search ..."> </form> </li> <li> <a class="tuHeaderLink" href="/repositum/information"> <u class=""> ABOUT REPOSITUM </u> </a> </li> <li> <a class="tuHeaderLink" href="https://colab.tuwien.ac.at/display/pubrepositum/" target="_blank"> <u class=""> HELP </u> </a> </li> </ul> </div> </div> </nav> </header> <div class="container-fluid" id="content"> <div class="row" id="firstRow"> <div class="sidebar"> <ul class="nav nav-sidebar"> <div id="loginElement" class="row"> <a id="loginAnchor" class="col-md-12" href="/mydspace"> Login <span class="fa fa-angle-right pull-right"></span> </a> </div> <li class="menuHeading text-uppercase"> <a href="/news" class="menuHeading"> News </a> </li> <li class="menuHeading text-uppercase"> <a class="menuHeading"> Browse by </a> </li> <li class=""> <a class="subMenuEntryLink" href="/repositum/community-list"> Publication Types </a> </li> <li class=""> <a class="subMenuEntryLink" href="/faculties"> Organizations </a> </li> <li class=""> <a class="subMenuEntryLink" href="/browse?type=rpname"> Researchers</a> </li> <li class=""> <a class="subMenuEntryLink" href="/browse?type=pjtitle"> Projects</a> </li> <li class=""> <a class="subMenuEntryLink" href="/academicpress"> TU Wien Academic Press </a> </li> <li class=""> <a class="subMenuEntryLink" href="/oaseries"> Open Access Series </a> </li> <li class=""> <a class="subMenuEntryLink" href="/simple-search?location=theses&rpp=25&sort_by=bi_sort_2_sort&order=DESC"> Theses </a> </li> <li class=""> <a class="subMenuEntryLink" href="/simple-search?location=digitised-works&rpp=50&sort_by=bi_sort_2_sort&order=DESC"> Digitised Works </a> </li> <li class=""> <a class="subMenuEntryLink" href="/browse?type=dateissued&rpp=25&sort_by=2&order=DESC"> Year of Publication</a> </li> </ul> </div> <div class="col-sm-12" id="main"> <div class="" id="contentContainer"> <div class="row"> <script type='text/javascript' src='/static/js/abbreviatetext.js'></script> <div class="row" id="itemPageFirstRow"> <div class="col-sm-12 col-md-12 col-lg-8"> </div> </div> <div class="row"> <div id="wrapperDisplayItem" class="col-lg-8 col-md-8"> <div class="row"> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Record link: </div> <div class="col-md-8 col-sm-8 metadataFieldValue"><a href="http://hdl.handle.net/20.500.12708/81367">http://hdl.handle.net/20.500.12708/81367</a><br /><a href="https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_38">https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_38</a></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row title-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Title: </div> <div class="col-md-8 col-sm-8 metadataFieldValue"><a href="/handle/20.500.12708/81367">Reactive Synthesis Modulo Theories using Abstraction Refinement</a></div> <div class="col-md-1 metadataLangValue">en</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Citation: </div> <div class="col-md-8 col-sm-8 metadataFieldValue"><div class="csl-bib-body"> <div class="csl-entry">Maderbacher, B., & Bloem, R. (2022). Reactive Synthesis Modulo Theories using Abstraction Refinement. In A. Griggio & N. Rungta (Eds.), <i>Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022</i> (pp. 315–324). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_38</div> </div></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">reposiTUm DOI: </div> <div class="col-md-8 col-sm-8 metadataFieldValue"><a href="https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_38">10.34727/2022/isbn.978-3-85448-053-2_38</a></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">CatalogPlus: </div> <div class="col-md-8 col-sm-8 metadataFieldValue"><a href="https://permalink.catalogplus.tuwien.at/AC17204234">AC17204234</a></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Publication Type: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">Inproceedings - Full-Paper Contribution</div> <div class="col-md-1 metadataLangValue">en</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Language: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">English</div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Authors: </div> <div class="col-md-8 col-sm-8 metadataFieldValue"><a href="/browse?type=author&authority=rp68314" class="authority author">Maderbacher, Benedikt</a> <a href="/cris/rp/rp68314" class="authority"><span data-toggle="tooltip" data-placement="top" title="External Staff" class="fa fa-user externalstaff" style="color:gray"></span></a><a target="_blank" href="https://orcid.org/0000-0002-5834-352X" class="authority"><span class="sm-orcid-icon" data-toggle="tooltip" data-placement="top" title="Orcid: 0000-0002-5834-352X"></span></a><br /><a href="/browse?type=author&authority=rp68315" class="authority author">Bloem, Roderick</a> <a href="/cris/rp/rp68315" class="authority"><span data-toggle="tooltip" data-placement="top" title="External Staff" class="fa fa-user externalstaff" style="color:gray"></span></a><a target="_blank" href="https://orcid.org/0000-0002-1411-5744" class="authority"><span class="sm-orcid-icon" data-toggle="tooltip" data-placement="top" title="Orcid: 0000-0002-1411-5744"></span></a></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Editors: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">Griggio, Alberto <a href="/cris/rp/rp68190" class="authority"><span data-toggle="tooltip" data-placement="top" title="External Staff" class="fa fa-user externalstaff" style="color:gray"></span></a><br />Rungta, Neha <a href="/cris/rp/rp68191" class="authority"><span data-toggle="tooltip" data-placement="top" title="External Staff" class="fa fa-user externalstaff" style="color:gray"></span></a></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Organisational Unit: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">E192-04 - Forschungsbereich Formal Methods in Systems Engineering <a href="/cris/ou/ou00499" class="authority"><span class="fa fa-university"></span></a></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Series: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">Conference Series: Formal Methods in Computer-Aided Design <a href="/cris/tuwseries/tuwseries00304" class="authority"><span class="fa fa-info"></span> </a></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Published in: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 <a href="/cris/books/books56662" class="authority"><span class="fa fa-book"></span></a></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Date (published): </div> <div class="col-md-8 col-sm-8 metadataFieldValue">Oct-2022</div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Number of Pages: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">10</div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Publisher: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">TU Wien Academic Press, Wien<br/></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Peer reviewed: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">Yes</div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Keywords: </div> <div class="col-md-8 col-sm-8 metadataFieldValue">formale Methode</div><div class="col-md-1 metadataLangValue">de</div></div><div class="row metadata-middle-row-start metadata-middle-row-end"><div class="col-md-3 col-sm-4 metadataFieldLabel"> </div><div class="col-md-8 col-sm-8 metadataFieldValue">formal methods</div> <div class="col-md-1 metadataLangValue">en</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">Linked records in reposiTUm: has part: </div> <div class="col-md-8 col-sm-8 metadataFieldValue"><a href="https://doi.org/10.34727/2022/isbn.978-3-85448-053-2">10.34727/2022/isbn.978-3-85448-053-2</a></div> <div class="col-md-1 metadataLangValue">-</div> </div> <div class="row metadata-row"> <div class="col-md-3 col-sm-4 metadataFieldLabel">License: </div> <div class="col-md-8 col-sm-8 metadataFieldValue"><a href="http://creativecommons.org/licenses/by/4.0/"><img src="/cris/do/fileservice/licences00482/261/?filename=cc-by.png" style="max-width:88px" alt="CC BY 4.0" title="Creative Commons Attribution 4.0 International"> CC BY 4.0</a></div> <div class="col-md-1 metadataLangValue">en</div> </div> <div class="row metadata-row"><div class="col-md-3 col-sm-4 metadataFieldLabel">Appears in Collections:</div><div class="col-md-8 col-sm-8 metadataFieldValue"><a href="/handle/20.500.12708/8">Open Access Series</a><br/><a href="/handle/20.500.12708/7">Conference Paper</a><br/></div><div class="col-md-1 metadataLangValue"></div></div> </div><br/> <div class="item-bitstream-grid-container"> <div class="item-bitstream-grid-thumbnail"> <a target="_blank" href="/bitstream/20.500.12708/81367/1/Maderbacher-2022-Reactive%20Synthesis%20Modulo%20Theories%20using%20Abstraction%20Ref...-vor.pdf"> <img data-thumbnail_type="withFrame" name="item-bitstream-grid-thumbnail" src="/retrieve/195203/Maderbacher-2022-Reactive%20Synthesis%20Modulo%20Theories%20using%20Abstraction%20Ref...-vor.pdf.jpg" alt="Thumbnail"> </a> </div> <div class="item-bitstream-grid-bitstream-type"> <a href="/bitstream/20.500.12708/81367/1/Maderbacher-2022-Reactive%20Synthesis%20Modulo%20Theories%20using%20Abstraction%20Ref...-vor.pdf" target="_blank"> Fulltext (Version of Record (published version)) </a> </div> <div class="item-bitstream-grid-file-format"> Adobe PDF </div> <div class="item-bitstream-grid-file-size"> (637.68 kB) </div> <div class="item-bitstream-grid-description"> </div> <div class="item-bitstream-grid-license-info"> <div class="item-bitstream-grid-license-info-flex-container"> <div class="item-bitstream-grid-license-info-flex-container-horizontal"> <img src="/image/open-access.png" height="22px" width="15px" title="Open Access" alt="Open Access"> <a href="http://creativecommons.org/licenses/by/4.0/" id="item-bitstream-license-link-195140" title="Creative Commons Attribution 4.0 International" data-toggle="tooltip" data-placement="right"> CC BY 4.0 </a> </div> </div> </div> </div> <hr> <div class="navigationButtonContainer"> <a class="btn btn-primary" href="/handle/20.500.12708/81367?mode=full"> Show full item record </a> </div> <div> </div> </div> <div id="panel-list-right" class="col-lg-4 col-md-4 col-sm-12"> <div class="row"> </div> <div class="row"> <script type="text/javascript"> j(document).ready(function () { var obj = JSON.parse('{"link":"https://repositum.tuwien.at/cris/stats/item.html?handle\u003d20.500.12708/81367"}'); j("div").data("moreLink", obj); j("#metric-counter-view").wrap(function () { return "<a target='_blank' href='" + j("div").data("moreLink").link + "'></a>"; }).append(" <i class='fa fa-info-circle' data-toggle='tooltip' title='Get updated citations from database'></i>"); jQuery('[data-toggle="tooltip"]').tooltip(); }); </script> <div class="col-lg-12 col-md-12 col-sm-8 box-view"> <div class="media view"> <div class="media-left"> <i class="fa fa-eye"></i> </div> <div class="media-body text-center"> <h4 class="media-heading">Page view(s) </h4> <span id="metric-counter-view" class="metric-counter"> 554 </span> </div> <div class="row"> <div class="col-lg-12 text-center small"> checked on Nov 21, 2023 </div> </div> </div> </div> <script type="text/javascript"> j(document).ready(function () { var obj = JSON.parse('{"link":"https://repositum.tuwien.at/cris/stats/item.html?handle\u003d20.500.12708/81367\u0026amp;type\u003dbitstream"}'); j("div").data("moreLink", obj); j("#metric-counter-download").wrap(function () { return "<a target='_blank' href='" + j("div").data("moreLink").link + "'></a>"; }).append(" <i class='fa fa-info-circle' data-toggle='tooltip' title='Get updated citations from database'></i>"); jQuery('[data-toggle="tooltip"]').tooltip(); }); </script> <div class="col-lg-12 col-md-12 col-sm-8 box-download"> <div class="media download"> <div class="media-left"> <i class="fa fa-cloud-download"></i> </div> <div class="media-body text-center"> <h4 class="media-heading">Download(s) </h4> <span id="metric-counter-download" class="metric-counter"> 160 </span> </div> <div class="row"> <div class="col-lg-12 text-center small"> checked on Nov 21, 2023 </div> </div> </div> </div> <div class="col-lg-12 col-md-12 col-sm-8"> <div class="media google"> <div class="media-left"> <img src="/image/google_scholar_logo.png" width="50" height="50" /> </div> <div id="googleCitedResult" class="media-body text-center"> <h4 class="media-heading">Google Scholar<sup>TM</sup><br/></h4> <span class="metric-counter"> <a data-toggle="tooltip" target="_blank" title="Search Google Scholar" href="https://scholar.google.com/scholar?as_q=&as_epq=Reactive+Synthesis+Modulo+Theories+using+Abstraction+Refinement&as_occt=title"> Check</a> </span> </div> </div> </div> <br class="visible-lg" /> </div> <div class="modal fade" id="dialogPMC" role="dialog" aria-labelledby="myModalLabel" aria-hidden="true"> <div class="modal-dialog"> <div class="modal-content"> </div> </div> </div> </div> </div> </div> </div> </div> </div> </div> <footer id="footer" > <script type="text/javascript">  </script> <div class="navbar navbar-default" id="footerContent"> <div id="footerContainer"> <p class="navbar-text pull-left">© <span id="year"></span> TU Wien <a href="#"></a> </p> <p class="navbar-text pull-right"> <a class="footerLink" href="https://www.tuwien.at/index.php?eID=dms&s=4&path=Documents/Data%20Protection%20Declaration%20Other/Data_Protection_Information_reposiTUm.pdf"> Data Protection Declaration </a> </p> <p class="navbar-text pull-right"> <a class="footerLink" href="javascript:linkTo_UnCryptMailto('nbjmup;sfqptjuvnAuvxjfo/bd/bu');">Support</a> </p> <p class="navbar-text pull-right"> <a class="footerLink" href="/repositum/policies">Policies</a> </p> <p class="navbar-text pull-right"> <a class="footerLink" href="https://www.tuwien.at/en/tu-wien/contact/legal-notice/"> Legal Notice </a> </p> <p class="navbar-text pull-right"> </p> </div> </div> </footer> </body> </html>

CINXE.COM

reposiTUm: Reactive Synthesis Modulo Theories using Abstraction Refinement