References

  1. Luca de Alfaro & Pritam Roy (2010): Solving games via three-valued abstraction refinement. Inf. Comput. 208(6), pp. 666–676, doi:10.1016/j.ic.2009.05.007.
  2. Gilles Audemard & Laurent Simon (2009): Predicting Learnt Clauses Quality in Modern SAT Solvers. In: IJCAI, pp. 399–404. Available at http://ijcai.org/Proceedings/09/Papers/074.pdf.
  3. Tomás Babiak, Mojmír Kretínský, Vojtech Rehák & Jan Strejcek (2012): LTL to Büchi Automata Translation: Fast and More Deterministic. In: TACAS, LNCS 7214. Springer, pp. 95–109, doi:10.1007/978-3-642-28756-5_8.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. Roderick Bloem, Swen Jacobs & Ayrat Khalimov (2014): Parameterized Synthesis Case Study: AMBA AHB. In: SYNT, EPTCS 157, pp. 68–83, doi:10.4204/EPTCS.157.9.
  9. 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.
  10. 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.
  11. 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.
  12. Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2014): AbsSynthe: abstract synthesis from succinct safety specifications. In: SYNT, EPTCS 157. Open Publishing Association, pp. 100–116, doi:10.4204/EPTCS.157.11.
  13. Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2015): Compositional Algorithms for Succinct Safety Games. In: SYNT, EPTCS 202. Open Publishing Association, pp. 98–111, doi:10.4204/EPTCS.202.7.
  14. Jerry R. Burch, Edmund M. Clarke & David E. Long (1991): Symbolic Model Checking with Partitioned Transistion Relations. In: VLSI, pp. 49–58.
  15. Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer, Danilo Vendraminetto, Armin Biere & Keijo Heljanko (2016): Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks. Journal on Satisfiability, Boolean Modeling and Computation 9, pp. 135–172. Available at https://www.satassociation.org/jsat/index.php/jsat/article/download/129/111.
  16. Alonzo Church (1962): Logic, arithmetic and automata. In: Proceedings of the international congress of mathematicians, pp. 23–35.
  17. 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.
  18. Rüdiger Ehlers (2012): Symbolic bounded synthesis. Formal Methods in System Design 40(2), pp. 232–262, doi:10.1007/s10703-011-0137-x.
  19. Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe & Leander Tentrup (2015): Encodings of Reactive Synthesis. In: Proceedings of QUANTIFY. Available at http://fmv.jku.at/quantify15/Faymonville-et-al-QUANTIFY2015.pdf.
  20. Bernd Finkbeiner & Swen Jacobs (2012): Lazy Synthesis. In: VMCAI, LNCS 7148. Springer, pp. 219–234, doi:10.1007/978-3-642-27940-9_15.
  21. 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.
  22. Bernd Finkbeiner & Sven Schewe (2013): Bounded synthesis. STTT 15(5-6), pp. 519–539, doi:10.1007/s10009-012-0228-z.
  23. Paul Gastin & Denis Oddoux (2001): Fast LTL to Büchi automata translation. In: CAV, LNCS 2102. Springer, pp. 53–65, doi:10.1007/3-540-44585-4_6.
  24. Yashdeep Godhal, Krishnendu Chatterjee & Thomas A. Henzinger (2013): Synthesis of AMBA AHB from formal specification: a case study. STTT 15(5-6), pp. 585–601, doi:10.1007/s10009-011-0207-9.
  25. Swen Jacobs (2014): Extended AIGER Format for Synthesis. CoRR abs/1405.5793. Available at http://arxiv.org/abs/1405.5793.
  26. Swen Jacobs & Roderick Bloem (2016): The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond. In: SYNT, this volume of EPTCS. Open Publishing Association. Open Publishing Association.
  27. 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 (2016): The First Reactive Synthesis Competition (SYNTCOMP 2014). STTT, doi:10.1007/s10009-016-0416-3. Published online first, journal issue to appear..
  28. Swen Jacobs, Roderick Bloem, Romain Brenguier, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2016): The Second Reactive Synthesis Competition (SYNTCOMP 2015). In: SYNT, EPTCS 202. Open Publishing Association, pp. 27–57, doi:10.4204/EPTCS.202.4.
  29. Swen Jacobs, Felix Klein & Sebastian Schirmer (2016): A High-Level LTL Synthesis Format: TLSF v1.1. In: SYNT 2016, this volume of EPTCS. Open Publishing Association. Open Publishing Association.
  30. 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.
  31. Barbara Jobstmann (2007): Applications and Optimizations for LTL Synthesis. Graz University of Technology.
  32. Barbara Jobstmann & Roderick Bloem (2006): Optimizations for LTL Synthesis. In: FMCAD. IEEE Computer Society, pp. 117–124, doi:10.1109/FMCAD.2006.22.
  33. Ayrat Khalimov (2015): Specification Format for Reactive Synthesis Problems. In: SYNT, EPTCS 202. Open Publishing Association, pp. 112–119, doi:10.4204/EPTCS.202.8.
  34. Ayrat Khalimov, Swen Jacobs & Roderick Bloem (2013): PARTY Parameterized Synthesis of Token Rings. In: CAV, LNCS 8044. Springer, pp. 928–933, doi:10.1007/978-3-642-39799-8_66.
  35. Ayrat Khalimov, Swen Jacobs & Roderick Bloem (2013): Towards Efficient Parameterized Synthesis. In: VMCAI, LNCS 7737. Springer, pp. 108–127, doi:10.1007/978-3-642-35873-9_9.
  36. Alexander Legg, Nina Narodytska & Leonid Ryzhyk (2016): A SAT-Based Counterexample Guided Method for Unbounded Synthesis. In: CAV (2), LNCS 9780. Springer, pp. 364–382, doi:10.1007/978-3-319-41540-6_20.
  37. 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.
  38. Leonardo Mendonça de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: TACAS, LNCS 4963. Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  39. Shipra Panda & Fabio Somenzi (1995): Who are the variables in your neighborhood. In: ICCAD. IEEE Computer Society / ACM, pp. 74–77, doi:10.1109/ICCAD.1995.479994.
  40. Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen & Natasha Sharygina (2013): PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification. In: LPAR, LNCS 8312. Springer, pp. 683–693, doi:10.1007/978-3-642-45221-5_45.
  41. 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.
  42. Richard Rudell (1993): Dynamic variable ordering for ordered binary decision diagrams. In: ICCAD. IEEE Computer Society, pp. 42–47, doi:10.1145/259794.259802.
  43. 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.
  44. M. Seidl & R. Könighofer (2014): Partial witnesses from preprocessed quantified Boolean formulas. In: DATE'14. IEEE, pp. 1–6. Available at http://dx.doi.org/10.7873/DATE2014.162.
  45. Fabio Somenzi (1999): Binary Decision Diagrams. In: Calculational system design 173. IOS Press, pp. 303.
  46. Leander Tentrup (2016): Solving QBF by Abstraction. CoRR abs/1604.06752. Available at http://arxiv.org/abs/1604.06752.
  47. Cong Tian, Jun Song, Zhenhua Duan & Zhao Duan (2015): LtlNfBa: Making LTL Translation More Practical. In: SOFL+MSVL, LNCS 9559. Springer, pp. 179–194, doi:10.1007/978-3-319-31220-0_13.
  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