{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:44:56Z","timestamp":1704455096684},"reference-count":43,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.202.4","type":"journal-article","created":{"date-parts":[[2016,2,1]],"date-time":"2016-02-01T23:24:58Z","timestamp":1454369098000},"page":"27-57","source":"Crossref","is-referenced-by-count":15,"title":["The Second Reactive Synthesis Competition (SYNTCOMP 2015)"],"prefix":"10.4204","volume":"202","author":[{"given":"Swen","family":"Jacobs","sequence":"first","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}]},{"given":"Roderick","family":"Bloem","sequence":"additional","affiliation":[{"name":"Graz University of Technology, Austria"}]},{"given":"Romain","family":"Brenguier","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Libre de Bruxelles, Brussels, Belgium"}]},{"given":"Robert","family":"K\u00f6nighofer","sequence":"additional","affiliation":[{"name":"Graz University of Technology, Austria"}]},{"given":"Guillermo A.","family":"P\u00e9rez","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Libre de Bruxelles, Brussels, Belgium"}]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Libre de Bruxelles, Brussels, Belgium"}]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and Carnegie Mellon University, Pittsburgh, USA"}]},{"given":"Ocan","family":"Sankur","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Libre de Bruxelles, Brussels, Belgium"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[{"name":"Johannes-Kepler-University, Linz, Austria"}]},{"given":"Leander","family":"Tentrup","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}]},{"given":"Adam","family":"Walker","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia"}]}],"member":"2720","published-online":{"date-parts":[[2016,2,2]]},"reference":[{"key":"dealfaro","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-74407-8_6","article-title":"Solving Games Via Three-Valued Abstraction Refinement","volume-title":"CONCUR","volume":"4703","author":"de Alfaro","year":"2007"},{"issue":"2","key":"AlurMN05","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/s10009-004-0179-0","article-title":"Symbolic computational techniques for solving games","volume":"7","author":"Alur","year":"2005","journal-title":"STTT"},{"key":"BalintDGGKR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1007\/978-3-642-25566-3_46","article-title":"EDACC - An Advanced Platform for the Experiment Design, Administration and Analysis of Empirical Algorithms","volume-title":"LION 5. Selected Papers","volume":"6683","author":"Balint","year":"2011"},{"key":"aiger","volume-title":"AIGER Format and Toolbox","author":"Biere"},{"key":"HWMCC","volume-title":"Hardware Model Checking Competition","author":"Biere"},{"key":"BloemEKKL14","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/FMCAD.2014.6987592","article-title":"SAT-based methods for circuit synthesis","volume-title":"FMCAD'14","author":"Bloem","year":"2014"},{"issue":"3","key":"BloemJPPS12","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","article-title":"Synthesis of Reactive(1) designs","volume":"78","author":"Bloem","year":"2012","journal-title":"J. Comput. Syst. Sci."},{"key":"BloemKS14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54013-4_1","article-title":"SAT-Based Synthesis Methods for Safety Specs","volume-title":"VMCAI","volume":"8318","author":"Bloem","year":"2014"},{"issue":"4","key":"BloemGJPPW07","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","article-title":"Specify, Compile, Run: Hardware from PSL","volume":"190","author":"Bloem","year":"2007","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"bbfjr12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","article-title":"Acacia+, a Tool for LTL Synthesis","volume-title":"CAV","volume":"7358","author":"Bohy","year":"2012"},{"key":"IIMC","volume-title":"Incremental Inductive Model Checker","author":"Bradley"},{"key":"Bradley11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","article-title":"SAT-Based Model Checking without Unrolling","volume-title":"VMCAI","volume":"6538","author":"Bradley","year":"2011"},{"key":"VIS","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","article-title":"VIS: A System for Verification and Synthesis","volume-title":"CAV","volume":"1102","author":"Brayton","year":"1996"},{"key":"abc","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","article-title":"ABC: An Academic Industrial-Strength Verification Tool","volume-title":"CAV","volume":"6174","author":"Brayton","year":"2010"},{"key":"BrenguierPRS14","series-title":"EPTCS","doi-asserted-by":"publisher","first-page":"100","DOI":"10.4204\/EPTCS.157.11","article-title":"AbsSynthe: abstract synthesis from succinct safety specifications","volume-title":"SYNT","volume":"157","author":"Brenguier","year":"2014"},{"key":"BrenguierPRS15","series-title":"this volume of EPTCS","article-title":"Compositional Algorithms for Succinct Safety Games","volume-title":"SYNT","author":"Brenguier","year":"2015"},{"issue":"8","key":"bryant86","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-Based Algorithms for Boolean Function Manipulation","volume":"35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Computers"},{"key":"BL69","doi-asserted-by":"publisher","first-page":"295","DOI":"10.2307\/1994916","article-title":"Solving sequential conditions by finite-state strategies","volume":"138","author":"B\u00fcchi","year":"1969","journal-title":"Trans. Amer. Math. Soc."},{"issue":"1","key":"ChenDSB12","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1109\/TRO.2011.2163434","article-title":"Formal Approach to the Deployment of Distributed Robotic Teams","volume":"28","author":"Chen","year":"2012","journal-title":"IEEE Transactions on Robotics"},{"key":"ChinchaliLTBM12","doi-asserted-by":"publisher","first-page":"5183","DOI":"10.1109\/ICRA.2012.6225257","article-title":"Towards formal synthesis of reactive controllers for dexterous robotic manipulation","volume-title":"ICRA","author":"Chinchali","year":"2012"},{"key":"Church62","first-page":"23","article-title":"Logic, arithmetic and automata","volume-title":"Proceedings of the international congress of mathematicians","author":"Church","year":"1962"},{"key":"Ehlers11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-19835-9_25","article-title":"Unbeast: Symbolic Bounded Synthesis","volume-title":"TACAS","volume":"6605","author":"Ehlers","year":"2011"},{"issue":"3","key":"EmersonC82","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","article-title":"Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons","volume":"2","author":"Emerson","year":"1982","journal-title":"Sci. Comput. Program."},{"key":"acacia","volume-title":"Acacia+","author":"Filiot"},{"key":"fjr10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-15643-4_10","article-title":"Compositional Algorithms for LTL Synthesis","volume-title":"ATVA","volume":"6252","author":"Filiot","year":"2010"},{"key":"FinkbeinerRS15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","article-title":"Algorithms for Model Checking HyperLTL and HyperCTL*","volume-title":"CAV","volume":"9206","author":"Finkbeiner","year":"2015"},{"issue":"9","key":"Huffman52","doi-asserted-by":"publisher","first-page":"1098","DOI":"10.1109\/JRPROC.1952.273898","article-title":"A Method for the Construction of Minimum-Redundancy Codes","volume":"40","author":"Huffman","year":"1952","journal-title":"Proceedings of the IRE"},{"key":"Jacobs15","article-title":"The First Reactive Synthesis Competition (SYNTCOMP 2014)","volume":"abs\/1506.08726","author":"Jacobs","year":"2015","journal-title":"CoRR"},{"key":"JobstmannB06","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1109\/FMCAD.2006.22","article-title":"Optimizations for LTL Synthesis","volume-title":"FMCAD","author":"Jobstmann","year":"2006"},{"key":"Khalimov15","series-title":"this volume of EPTCS","article-title":"Specification Format for Reactive Synthesis Problems","volume-title":"SYNT","author":"Khalimov","year":"2015"},{"issue":"6","key":"Kress-GazitFP09","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","article-title":"Temporal-Logic-Based Reactive Mission and Motion Planning","volume":"25","author":"Kress-Gazit","year":"2009","journal-title":"IEEE Transactions on Robotics"},{"key":"LonsingE14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-319-10428-7_38","article-title":"Incremental QBF Solving","volume-title":"CP","volume":"8656","author":"Lonsing","year":"2014"},{"key":"SMVSystem","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-1-4615-3190-6_4","article-title":"The SMV System","volume-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"MorgensternGS13","series-title":"LNCS 7940","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-38613-8_13","article-title":"Solving Games Using Incremental Induction","volume-title":"IFM'13","author":"Morgenstern","year":"2013"},{"key":"PnueliR89","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/75277.75293","article-title":"On the Synthesis of a Reactive Module","volume-title":"POPL","author":"Pnueli","year":"1989"},{"key":"Rabin69","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1090\/S0002-9947-1969-0246760-1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Trans. Amer. Math. Soc."},{"issue":"4","key":"Roussel11","first-page":"139","article-title":"Controlling a Solver Execution with the runsolver Tool","volume":"7","author":"Roussel","year":"2011","journal-title":"JSAT"},{"key":"Rudell93","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/259794.259802","article-title":"Dynamic variable ordering for ordered binary decision diagrams","volume-title":"ICCAD","author":"Rudell","year":"1993"},{"key":"RyzhykWKLRSV14","first-page":"661","article-title":"User-Guided Device Driver Synthesis","volume-title":"OSDI","author":"Ryzhyk","year":"2014"},{"key":"SeidlK14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.7873\/DATE2014.162","article-title":"Partial witnesses from preprocessed quantified Boolean formulas","volume-title":"DATE'14","author":"Seidl","year":"2014"},{"key":"somenzi99","article-title":"Binary Decision Diagrams","volume-title":"Calculational system design","volume":"173","author":"Somenzi","year":"1999"},{"key":"Thomas95","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-59042-0_57","article-title":"On the Synthesis of Strategies in Infinite Games","volume-title":"STACS","author":"Thomas","year":"1995"},{"issue":"12","key":"WuWLH14","doi-asserted-by":"publisher","first-page":"1846","DOI":"10.1109\/TCAD.2014.2363395","article-title":"A Counterexample-Guided Interpolant Generation Algorithm for SAT-Based Model Checking","volume":"33","author":"Wu","year":"2014","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2016,2,5]],"date-time":"2016-02-05T01:03:07Z","timestamp":1454634187000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1602.01171"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,2]]},"references-count":43,"URL":"https:\/\/doi.org\/10.4204\/eptcs.202.4","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,2]]}}}