@article(journals/fmsd/BalabanovJ12,
 author       = {Valeriy Balabanov and Jie{-}Hong R. Jiang},
 year         = {2012},
 title        = {Unified {QBF} certification and its applications},
 journal      = {Formal Methods in System Design},
 volume       = {41},
 number       = {1},
 pages        = {45--65},
 doi          = {10.1007/s10703-012-0152-6},
)
@inproceedings(conf/innovations/BeyersdorffBC16,
 author       = {Olaf Beyersdorff and Ilario Bonacina and Leroy Chew},
 year         = {2016},
 title        = {Lower Bounds: From Circuits to {QBF} Proof Systems},
 booktitle    = {Proceedings of {ITCS}},
 publisher    = {{ACM}},
 pages        = {249--260},
 doi          = {10.1145/2840728.2840740},
)
@inproceedings(conf/vmcai/BloemKS14,
 author       = {Roderick Bloem and Robert K{\"{o}}nighofer and Martina Seidl},
 year         = {2014},
 title        = {{SAT}-Based Synthesis Methods for Safety Specs},
 booktitle    = {Proceedings of {VMCAI}},
 series       = {LNCS},
 volume       = {8318},
 publisher    = {Springer},
 pages        = {1--20},
 doi          = {10.1007/978-3-642-54013-4_1},
)
@article(journals/constraints/EglySW09,
 author       = {Uwe Egly and Martina Seidl and Stefan Woltran},
 year         = {2009},
 title        = {A solver for {QBFs} in negation normal form},
 journal      = {Constraints},
 volume       = {14},
 number       = {1},
 pages        = {38--79},
 doi          = {10.1007/s10601-008-9055-y},
)
@inproceedings(conf/tacas/FaymonvilleFRT17,
 author       = {Peter Faymonville and Bernd Finkbeiner and Markus N. Rabe and Leander Tentrup},
 year         = {2017},
 title        = {Encodings of Bounded Synthesis},
 booktitle    = {Proceedings of {TACAS}},
 series       = {LNCS},
 volume       = {10205},
 pages        = {354--370},
 doi          = {10.1007/978-3-662-54577-5_20},
)
@inproceedings(conf/cav/FaymonvilleFT17,
 author       = {Peter Faymonville and Bernd Finkbeiner and Leander Tentrup},
 year         = {2017},
 title        = {{BoSy}: An Experimentation Framework for Bounded Synthesis},
 booktitle    = {Proceedings of {CAV}},
 series       = {LNCS},
 volume       = {10427},
 publisher    = {Springer},
 pages        = {325--332},
 doi          = {10.1007/978-3-319-63390-9_17},
)
@inproceedings(conf/birthday/Finkbeiner15,
 author       = {Bernd Finkbeiner},
 year         = {2015},
 title        = {Bounded Synthesis for {Petri} Games},
 booktitle    = {Proceedings of Correct System Design},
 series       = {LNCS},
 volume       = {9360},
 publisher    = {Springer},
 pages        = {223--237},
 doi          = {10.1007/978-3-319-23506-6_15},
)
@inproceedings(journals/corr/abs-1711-10637,
 author       = {Bernd Finkbeiner and Manuel Gieseking and Hecking{-}Harbusch, Jesko and Ernst{-}R{\"{u}}diger Olderog},
 year         = {2017},
 title        = {Symbolic vs. Bounded Synthesis for Petri Games},
 booktitle    = {Proceedings of {SYNT@CAV}},
 series       = {EPTCS},
 volume       = {260},
 pages        = {23--43},
 doi          = {10.4204/EPTCS.260.5},
)
@inproceedings(conf/cav/FinkbeinerGO15,
 author       = {Bernd Finkbeiner and Manuel Gieseking and Ernst{-}R{\"{u}}diger Olderog},
 year         = {2015},
 title        = {Adam: Causality-Based Synthesis of Distributed Systems},
 booktitle    = {Proceedings of {CAV}},
 series       = {LNCS},
 volume       = {9206},
 publisher    = {Springer},
 pages        = {433--439},
 doi          = {10.1007/978-3-319-21690-4_25},
)
@article(journals/iandc/FinkbeinerO17,
 author       = {Bernd Finkbeiner and Ernst{-}R{\"{u}}diger Olderog},
 year         = {2017},
 title        = {Petri games: Synthesis of distributed systems with causal memory},
 journal      = {Inf. Comput.},
 volume       = {253},
 pages        = {181--203},
 doi          = {10.1016/j.ic.2016.07.006},
)
@inproceedings(conf/tacas/FinkbeinerT14,
 author       = {Bernd Finkbeiner and Leander Tentrup},
 year         = {2014},
 title        = {Detecting Unrealizable Specifications of Distributed Systems},
 booktitle    = {Proceedings of {TACAS}},
 series       = {LNCS},
 volume       = {8413},
 publisher    = {Springer},
 pages        = {78--92},
 doi          = {10.1007/978-3-642-54862-8_6},
)
@article(journals/corr/FinkbeinerT15,
 author       = {Bernd Finkbeiner and Leander Tentrup},
 year         = {2015},
 title        = {Detecting Unrealizability of Distributed Fault-tolerant Systems},
 journal      = {Logical Methods in Computer Science},
 volume       = {11},
 number       = {3},
 doi          = {10.2168/LMCS-11(3:12)2015},
)
@inproceedings(conf/aaai/GoultiaevaB10,
 author       = {Alexandra Goultiaeva and Fahiem Bacchus},
 year         = {2010},
 title        = {Exploiting {QBF} Duality on a Circuit Representation},
 booktitle    = {Proceedings of {AAAI}},
 publisher    = {{AAAI} Press},
)
@inproceedings(conf/sat/GoultiaevaIB09,
 author       = {Alexandra Goultiaeva and Vicki Iverson and Fahiem Bacchus},
 year         = {2009},
 title        = {Beyond {CNF:} {A} Circuit-Based {QBF} Solver},
 booktitle    = {Proceedings of {SAT}},
 series       = {LNCS},
 volume       = {5584},
 publisher    = {Springer},
 pages        = {412--426},
 doi          = {10.1007/978-3-642-02777-2_38},
)
@inproceedings(conf/date/GoultiaevaSB13,
 author       = {Alexandra Goultiaeva and Martina Seidl and Armin Biere},
 year         = {2013},
 title        = {Bridging the gap between dual propagation and {CNF}-based {QBF} solving},
 booktitle    = {Proceedings of {DATE}},
 publisher    = {IEEE},
 pages        = {811--814},
 doi          = {10.7873/DATE.2013.172},
)
@inproceedings(conf/fmcad/HeuleSB14,
 author       = {Marijn Heule and Martina Seidl and Armin Biere},
 year         = {2014},
 title        = {Efficient extraction of {Skolem} functions from {QRAT} proofs},
 booktitle    = {Proceedings of {FMCAD}},
 publisher    = {IEEE},
 pages        = {107--114},
 doi          = {10.1109/FMCAD.2014.6987602},
)
@inproceedings(journals/corr/abs-1711-11439,
 author       = {Swen Jacobs and Nicolas Basset and Roderick Bloem and Romain Brenguier and Maximilien Colange and Peter Faymonville and Bernd Finkbeiner and Ayrat Khalimov and Felix Klein and Thibaud Michaud and Guillermo A. P{\'{e}}rez and Jean{-}Fran{\c{c}}ois Raskin and Ocan Sankur and Leander Tentrup},
 year         = {2017},
 title        = {The 4th Reactive Synthesis Competition {(SYNTCOMP} 2017): Benchmarks, Participants {\&} Results},
 booktitle    = {Proceedings of {SYNT@CAV}},
 series       = {EPTCS},
 volume       = {260},
 pages        = {116--143},
 doi          = {10.4204/EPTCS.260.10},
)
@article(journals/sttt/JacobsBBEHKPRRS17,
 author       = {Swen Jacobs and Roderick Bloem and Romain Brenguier and R{\"{u}}diger Ehlers and Timotheus Hell and Robert K{\"{o}}nighofer and Guillermo A. P{\'{e}}rez and Jean{-}Fran{\c{c}}ois Raskin and Leonid Ryzhyk and Ocan Sankur and Martina Seidl and Leander Tentrup and Adam Walker},
 year         = {2017},
 title        = {The first reactive synthesis competition {(SYNTCOMP} 2014)},
 journal      = {STTT},
 volume       = {19},
 number       = {3},
 pages        = {367--390},
 doi          = {10.1007/s10009-016-0416-3},
)
@inproceedings(journals/corr/JacobsBBK0KKLNP16,
 author       = {Swen Jacobs and Roderick Bloem and Romain Brenguier and Ayrat Khalimov and Felix Klein and Robert K{\"{o}}nighofer and Jens Kreber and Alexander Legg and Nina Narodytska and Guillermo A. P{\'{e}}rez and Jean{-}Fran{\c{c}}ois Raskin and Leonid Ryzhyk and Ocan Sankur and Martina Seidl and Leander Tentrup and Adam Walker},
 year         = {2016},
 title        = {The 3rd Reactive Synthesis Competition {(SYNTCOMP} 2016): Benchmarks, Participants {\&} Results},
 booktitle    = {Proceedings of {SYNT@CAV}},
 series       = {EPTCS},
 volume       = {229},
 pages        = {149--177},
 doi          = {10.4204/EPTCS.229.12},
)
@inproceedings(conf/sat/Janota18,
 author       = {Mikol{\'{a}}s Janota},
 year         = {2018},
 title        = {Circuit-Based Search Space Pruning in {QBF}},
 booktitle    = {Proceedings of {SAT}},
 series       = {LNCS},
 volume       = {10929},
 publisher    = {Springer},
 pages        = {187--198},
 doi          = {10.1007/978-3-319-94144-8\_12},
)
@inproceedings(conf/aaai/Janota18,
 author       = {Mikol{\'{a}}s Janota},
 year         = {2018},
 title        = {Towards Generalization in {QBF} Solving via Machine Learning},
 booktitle    = {Proceedings of {AAAI}},
 publisher    = {{AAAI} Press},
)
@article(journals/ai/JanotaKMC16,
 author       = {Mikol{\'{a}}s Janota and William Klieber and Marques{-}Silva, Joao and Edmund M. Clarke},
 year         = {2016},
 title        = {Solving {QBF} with counterexample guided refinement},
 journal      = {Artif. Intell.},
 volume       = {234},
 pages        = {1--25},
 doi          = {10.1016/j.artint.2016.01.004},
)
@inproceedings(conf/ijcai/JanotaM15,
 author       = {Mikol{\'{a}}s Janota and Marques{-}Silva, Joao},
 year         = {2015},
 title        = {Solving {QBF} by Clause Selection},
 booktitle    = {Proceedings of {IJCAI}},
 publisher    = {{AAAI} Press},
 pages        = {325--331},
)
@inproceedings(conf/epia/JanotaM17,
 author       = {Mikol{\'{a}}s Janota and Marques{-}Silva, Joao},
 year         = {2017},
 title        = {An Achilles' Heel of Term-Resolution},
 booktitle    = {Proceedings of {EPIA}},
 series       = {LNCS},
 volume       = {10423},
 publisher    = {Springer},
 pages        = {670--680},
 doi          = {10.1007/978-3-319-65340-2_55},
)
@inproceedings(conf/sat/KlieberSGC10,
 author       = {William Klieber and Samir Sapra and Sicun Gao and Edmund M. Clarke},
 year         = {2010},
 title        = {A Non-prenex, Non-clausal {QBF} Solver with Game-State Learning},
 booktitle    = {Proceedings of {SAT}},
 series       = {LNCS},
 volume       = {6175},
 publisher    = {Springer},
 pages        = {128--142},
 doi          = {10.1007/978-3-642-14186-7_12},
)
@inproceedings(conf/sat/LonsingB08,
 author       = {Florian Lonsing and Armin Biere},
 year         = {2008},
 title        = {Nenofex: Expanding {NNF} for {QBF} Solving},
 booktitle    = {Proceedings of {SAT}},
 series       = {LNCS},
 volume       = {4996},
 publisher    = {Springer},
 pages        = {196--210},
 doi          = {10.1007/978-3-540-79719-7_19},
)
@inproceedings(conf/sat/NiemetzPLSB12,
 author       = {Aina Niemetz and Mathias Preiner and Florian Lonsing and Martina Seidl and Armin Biere},
 year         = {2012},
 title        = {Resolution-Based Certificate Extraction for {QBF}},
 booktitle    = {Proceedings of {SAT}},
 series       = {LNCS},
 volume       = {7317},
 publisher    = {Springer},
 pages        = {430--435},
 doi          = {10.1007/978-3-642-31612-8_33},
)
@inproceedings(conf/sat/PeitlSS17,
 author       = {Tom{\'{a}}s Peitl and Friedrich Slivovsky and Stefan Szeider},
 year         = {2017},
 title        = {Dependency Learning for {QBF}},
 booktitle    = {Proceedings of {SAT}},
 series       = {LNCS},
 volume       = {10491},
 publisher    = {Springer},
 pages        = {298--313},
 doi          = {10.1007/978-3-319-66263-3_19},
)
@inproceedings(conf/date/PigorschS09,
 author       = {Florian Pigorsch and Christoph Scholl},
 year         = {2009},
 title        = {Exploiting structure in an {AIG} based {QBF} solver},
 booktitle    = {Proceedings of {DATE}},
 publisher    = {IEEE},
 pages        = {1596--1601},
 doi          = {10.1109/DATE.2009.5090919},
)
@article(journals/jsc/PlaistedG86,
 author       = {David A. Plaisted and Steven Greenbaum},
 year         = {1986},
 title        = {A Structure-Preserving Clause Form Translation},
 journal      = {J. Symb. Comput.},
 volume       = {2},
 number       = {3},
 pages        = {293--304},
 doi          = {10.1016/S0747-7171(86)80028-1},
)
@inproceedings(conf/sat/Pulina16,
 author       = {Luca Pulina},
 year         = {2016},
 title        = {The Ninth {QBF} Solvers Evaluation - Preliminary Report},
 booktitle    = {Proceedings of {QBF@SAT}},
 series       = {{CEUR} Workshop Proceedings},
 volume       = {1719},
 publisher    = {CEUR-WS.org},
 pages        = {1--13},
)
@inproceedings(conf/fmcad/RabeT15,
 author       = {Markus N. Rabe and Leander Tentrup},
 year         = {2015},
 title        = {{CAQE:} {A} Certifying {QBF} Solver},
 booktitle    = {Proceedings of {FMCAD}},
 publisher    = {IEEE},
 pages        = {136--143},
)
@inproceedings(conf/sat/SoosNC09,
 author       = {Mate Soos and Karsten Nohl and Claude Castelluccia},
 year         = {2009},
 title        = {Extending {SAT} Solvers to Cryptographic Problems},
 booktitle    = {Proceedings of {SAT}},
 series       = {LNCS},
 volume       = {5584},
 publisher    = {Springer},
 pages        = {244--257},
 doi          = {10.1007/978-3-642-02777-2_24},
)
@inproceedings(conf/sat/Tentrup16,
 author       = {Leander Tentrup},
 year         = {2016},
 title        = {Non-prenex {QBF} Solving Using Abstraction},
 booktitle    = {Proceedings of {SAT}},
 series       = {LNCS},
 volume       = {9710},
 publisher    = {Springer},
 pages        = {393--401},
 doi          = {10.1007/978-3-319-40970-2_24},
)
@inproceedings(conf/cav/Tentrup17,
 author       = {Leander Tentrup},
 year         = {2017},
 title        = {On Expansion and Resolution in {CEGAR} Based {QBF} Solving},
 booktitle    = {Proceedings of {CAV}},
 series       = {LNCS},
 volume       = {10427},
 publisher    = {Springer},
 pages        = {475--494},
 doi          = {10.1007/978-3-319-63390-9\_25},
)
@inproceedings(conf/sat/TuHJ15,
 author       = {Kuan{-}Hua Tu and Tzu{-}Chien Hsu and Jie{-}Hong R. Jiang},
 year         = {2015},
 title        = {{QELL:} {QBF} Reasoning with Extended Clause Learning and Levelized {SAT} Solving},
 booktitle    = {Proceedings of {SAT}},
 series       = {LNCS},
 volume       = {9340},
 publisher    = {Springer},
 pages        = {343--359},
 doi          = {10.1007/978-3-319-24318-4_25},
)