References

  1. Termite Driver Synthesis Tool. http://ssrg.nicta.com.au/projects/TS/drivers/synthesis/.
  2. V3 - An Extensible Framework for Hardware Verification. http://dvlab.ee.ntu.edu.tw/~publication/V3/.
  3. Luca de Alfaro & Pritam Roy (2007): Solving Games Via Three-Valued Abstraction Refinement. In: CONCUR, LNCS 4703. Springer, pp. 74–89, doi:10.1007/978-3-540-74407-8_6.
  4. Rajeev Alur, P. Madhusudan & Wonhong Nam (2005): Symbolic computational techniques for solving games. STTT 7(2), pp. 118–128, doi:10.1007/s10009-004-0179-0.
  5. Adrian Balint, Daniel Diepold, Daniel Gall, Simon Gerber, Gregor Kapler & Robert Retz (2011): EDACC - An Advanced Platform for the Experiment Design, Administration and Analysis of Empirical Algorithms. In: LION 5. Selected Papers, LNCS 6683. Springer, pp. 586–599, doi:10.1007/978-3-642-25566-3_46.
  6. Armin Biere: AIGER Format and Toolbox, http://fmv.jku.at/aiger/.
  7. Armin Biere: Hardware Model Checking Competition, http://fmv.jku.at/hwmcc/.
  8. R. Bloem, U. Egly, P. Klampfl, R. Könighofer & F. Lonsing (2014): SAT-based methods for circuit synthesis. In: FMCAD'14. IEEE, pp. 31–34, doi:10.1109/FMCAD.2014.6987592.
  9. R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli & Y. Sa'ar (2012): Synthesis of Reactive(1) designs. J. Comput. Syst. Sci. 78(3), pp. 911–938, doi:10.1016/j.jcss.2011.08.007.
  10. R. Bloem, R. Könighofer & M. Seidl (2014): SAT-Based Synthesis Methods for Safety Specs. In: VMCAI, LNCS 8318. Springer, pp. 1–20, doi:10.1007/978-3-642-54013-4_1.
  11. Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007): Specify, Compile, Run: Hardware from PSL. Electr. Notes Theor. Comput. Sci. 190(4), pp. 3–16, doi:10.1016/j.entcs.2007.09.004.
  12. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2012): Acacia+, a Tool for LTL Synthesis. In: CAV, LNCS 7358. Springer, pp. 652–657, doi:10.1007/978-3-642-31424-7_45.
  13. Aaron Bradley, Fabio Somenzi, Michael Dooley, Zyad Hassan & Yan Zhang: Incremental Inductive Model Checker, http://ecee.colorado.edu/wpmu/iimc/.
  14. Aaron R. Bradley (2011): SAT-Based Model Checking without Unrolling. In: VMCAI, LNCS 6538. Springer, pp. 70–87, doi:10.1007/978-3-642-18275-4_7.
  15. Robert K. Brayton, Gary D. Hachtel, Alberto L. Sangiovanni-Vincentelli, Fabio Somenzi, Adnan Aziz, Szu-Tsung Cheng, Stephen A. Edwards, Sunil P. Khatri, Yuji Kukimoto, Abelardo Pardo, Shaz Qadeer, Rajeev K. Ranjan, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy & Tiziano Villa (1996): VIS: A System for Verification and Synthesis. In: CAV, LNCS 1102. Springer, pp. 428–432, doi:10.1007/3-540-61474-5_95.
  16. Robert K. Brayton & Alan Mishchenko (2010): ABC: An Academic Industrial-Strength Verification Tool. In: CAV, LNCS 6174. Springer, pp. 24–40, doi:10.1007/978-3-642-14295-6_5.
  17. Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2014): AbsSynthe: abstract synthesis from succinct safety specifications. In: SYNT, EPTCS 157, pp. 100–116, doi:10.4204/EPTCS.157.11.
  18. Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2015): Compositional Algorithms for Succinct Safety Games. In: SYNT, this volume of EPTCS. Open Publishing Association. Open Publishing Association.
  19. Randal E. Bryant (1986): Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), pp. 677–691, doi:10.1109/TC.1986.1676819.
  20. J.R. Büchi & L.H. Landweber (1969): Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, pp. 295–311, doi:10.2307/1994916.
  21. Yushan Chen, Xu Chu Ding, Alin Stefanescu & Calin Belta (2012): Formal Approach to the Deployment of Distributed Robotic Teams. IEEE Transactions on Robotics 28(1), pp. 158–171, doi:10.1109/TRO.2011.2163434.
  22. Sandeep Chinchali, Scott C. Livingston, Ufuk Topcu, Joel W. Burdick & Richard M. Murray (2012): Towards formal synthesis of reactive controllers for dexterous robotic manipulation. In: ICRA. IEEE, pp. 5183–5189, doi:10.1109/ICRA.2012.6225257.
  23. Alonzo Church (1962): Logic, arithmetic and automata. In: Proceedings of the international congress of mathematicians, pp. 23–35.
  24. Rüdiger Ehlers (2011): Unbeast: Symbolic Bounded Synthesis. In: TACAS, LNCS 6605. Springer, pp. 272–275, doi:10.1007/978-3-642-19835-9_25.
  25. E. Allen Emerson & Edmund M. Clarke (1982): Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Sci. Comput. Program. 2(3), pp. 241–266, doi:10.1016/0167-6423(83)90017-5.
  26. Emmanuel Filiot: Acacia+, http://lit2.ulb.ac.be/acaciaplus/.
  27. Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2010): Compositional Algorithms for LTL Synthesis. In: ATVA, LNCS 6252. Springer, pp. 112–127, doi:10.1007/978-3-642-15643-4_10.
  28. Bernd Finkbeiner, Markus N. Rabe & César Sánchez (2015): Algorithms for Model Checking HyperLTL and HyperCTL*. In: CAV, LNCS 9206. Springer, pp. 30–48, doi:10.1007/978-3-319-21690-4_3.
  29. David A. Huffman (1952): A Method for the Construction of Minimum-Redundancy Codes. Proceedings of the IRE 40(9), pp. 1098–1101, doi:10.1109/JRPROC.1952.273898.
  30. 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 (2015): The First Reactive Synthesis Competition (SYNTCOMP 2014). CoRR abs/1506.08726. Available at http://arxiv.org/abs/1506.08726.
  31. Barbara Jobstmann & Roderick Bloem (2006): Optimizations for LTL Synthesis. In: FMCAD. IEEE Computer Society, pp. 117–124, doi:10.1109/FMCAD.2006.22.
  32. Ayrat Khalimov: Aisy: Simple synthesis tool from AIGER circuits format.. https://bitbucket.org/art_haali/aisy-classroom.
  33. Ayrat Khalimov (2015): Specification Format for Reactive Synthesis Problems. In: SYNT, this volume of EPTCS. Open Publishing Association. Open Publishing Association.
  34. Hadas Kress-Gazit, Georgios E. Fainekos & George J. Pappas (2009): Temporal-Logic-Based Reactive Mission and Motion Planning. IEEE Transactions on Robotics 25(6), pp. 1370–1381, doi:10.1109/TRO.2009.2030225.
  35. Florian Lonsing & Uwe Egly (2014): Incremental QBF Solving. In: CP, LNCS 8656. Springer, pp. 514–530, doi:10.1007/978-3-319-10428-7_38.
  36. Kenneth L. McMillan (1993): The SMV System. In: Symbolic Model Checking. Springer, pp. 61–85, doi:10.1007/978-1-4615-3190-6_4.
  37. Kenneth L McMillan (1999): The SMV language. Technical Report. Cadence Berkeley Labs. Available at http://web.cs.wpi.edu/~kfisler/Courses/525V/S02/Readings/smv-cadence.pdf.
  38. A. Morgenstern, M. Gesell & K. Schneider (2013): Solving Games Using Incremental Induction. In: IFM'13, LNCS 7940. Springer, pp. 177–191, doi:10.1007/978-3-642-38613-8_13.
  39. Bryan O'Sullivan: Attoparsec. https://hackage.haskell.org/package/attoparsec.
  40. Amir Pnueli & Roni Rosner (1989): On the Synthesis of a Reactive Module. In: POPL. ACM Press, pp. 179–190, doi:10.1145/75277.75293.
  41. Michael O. Rabin (1969): Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, pp. 1–35, doi:10.1090/S0002-9947-1969-0246760-1.
  42. Olivier Roussel (2011): Controlling a Solver Execution with the runsolver Tool. JSAT 7(4), pp. 139–144. Available at http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_12_Roussel.pdf.
  43. Richard Rudell (1993): Dynamic variable ordering for ordered binary decision diagrams. In: ICCAD. IEEE Computer Society, pp. 42–47, doi:10.1145/259794.259802.
  44. Leonid Ryzhyk, Adam Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm & Mona Vij (2014): User-Guided Device Driver Synthesis. In: OSDI. USENIX Association, pp. 661–676. Available at https://www.usenix.org/conference/osdi14/technical-sessions/presentation/ryzhyk.
  45. M. Seidl & R. Könighofer (2014): Partial witnesses from preprocessed quantified Boolean formulas. In: DATE'14. IEEE, pp. 1–6, doi:10.7873/DATE2014.162.
  46. Fabio Somenzi (1999): Binary Decision Diagrams. In: Calculational system design 173. IOS Press, pp. 303.
  47. Wolfgang Thomas (1995): On the Synthesis of Strategies in Infinite Games. In: STACS, pp. 1–13, doi:10.1007/3-540-59042-0_57.
  48. Cheng-Yin Wu, Chi-An Wu, Chien-Yu Lai & Chung-Yang R. Haung (2014): A Counterexample-Guided Interpolant Generation Algorithm for SAT-Based Model Checking. IEEE Trans. on CAD of Integrated Circuits and Systems 33(12), pp. 1846–1858, doi:10.1109/TCAD.2014.2363395.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org