References

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