References

1. open-Promela compiler (Python package). Available at https://github.com/johnyf/openpromela.
2. Promela parser (Python package). Available at https://github.com/johnyf/promela.
3. Slugs instrumentation at tag synt_2015. Available at https://github.com/johnyf/slugs.
4. dd: Decision diagrams (Python package). Available at https://github.com/johnyf/dd.
5. omega: Symbolic and enumerated data structures and algorithms for manipulating ω-regular sets (Python package). Available at https://github.com/johnyf/omega.
6. Martín Abadi & Leslie Lamport (1994): Open systems in TLA. In: PODC, pp. 81–90, doi:10.1145/197917.197960.
7. Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak & Abhishek Udupa (2013): Syntax-guided synthesis. In: FMCAD, pp. 1–17, doi:10.1109/FMCAD.2013.6679385.
8. Rajeev Alur & Salvatore La Torre (2004): Deterministic generators and games for LTL fragments. ACM Trans. Comput. Logic 5(1), pp. 1–25, doi:10.1145/963927.963928.
9. ARM Ltd. (1999): AMBASpecification, Rev 2.0 edition. Available at http://www-micro.deis.unibo.it/~magagni/amba99.pdf.
10. Christel Baier & Joost-Pieter Katoen (2008): Principles of model checking. The MIT Press.
11. Michael Baldamus & Jochen Schröder-Babo (2001): P2B: A translation utility for linking Promela and symbolic model checking. In: SPIN, pp. 183–191, doi:10.1007/3-540-45139-0_11.
12. JiříBarnat, Luboš Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenčo, Petr Ročkai, Vladimír Štill & JiříWeiser (2013): DiVinE 3.0 – An explicit-state model checker for multithreaded C & C++ programs. In: CAV 8044, pp. 863–868, doi:10.1007/978-3-642-39799-8_60.
13. Vincent Beaudenon, Emmanuelle Encrenaz & Sami Taktak (2010): Data decision diagrams for promela systems analysis. STTT 12(5), pp. 337–352, doi:10.1007/s10009-010-0135-0.
14. David M. Beazley: PLY (Python Lex-Yacc) v3.4. Available at http://www.dabeaz.com/ply/ply.html.
15. Tewodros Beyene, Swarat Chaudhuri, Corneliu Popeea & Andrey Rybalchenko (2014): A constraint-based approach to solving games on infinite graphs. In: POPL, pp. 221–233, doi:10.1145/2535838.2535860.
16. Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan & Richard Seeber (2010): Ratsy–A new requirements analysis tool with synthesis. In: CAV, pp. 425–429, doi:10.1007/978-3-642-14295-6_37.
17. Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007): Interactive presentation: Automatic hardware synthesis from specifications: A case study. In: Design, Automation and Test in Europe (DATE), pp. 1188–1193. Available at http://dl.acm.org/citation.cfm?id=1266366.1266622.
18. Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007): Specify, compile, run: Hardware from PSL. ENTCS 190(4), pp. 3–16, doi:10.1016/j.entcs.2007.09.004.
19. Roderick Bloem, Swen Jacobs & Ayrat Khalimov (2014): Parameterized synthesis case study: AMBA AHB. In: Krishnendu Chatterjee, Rüdiger Ehlers & Susmit Jha: SYNT, EPTCS 157, pp. 68–83, doi:10.4204/EPTCS.157.9. Available at http://arxiv.org/abs/1407.6580v1.
20. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Yaniv Sa'ar (2012): Synthesis of reactive(1) designs. Journal of Computer and System Sciences (JCSS) 78(3), pp. 911–938, doi:10.1016/j.jcss.2011.08.007.
21. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2012): Acacia+, a tool for LTL synthesis. In: CAV, pp. 652–657, doi:10.1007/978-3-642-31424-7_45.
22. Manfred Broy (1986): A theory for nondeterminism, parallelism, communication, and concurrency. TCS 45(0), pp. 1–61, doi:10.1016/0304-3975(86)90040-X.
23. Randal E. Bryant (1986): Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), pp. 677–691, doi:10.1109/TC.1986.1676819.
24. Roberto Cavada, Alessandro Cimatti, Charles Arthur Jochim, Gavin Keighren, Emanuele Olivetti, Marco Pistore, Marco Roveri & Andrei Tchaltsev (2010): NuSMV 2.5 User Manual. Technical Report. Fondazione Bruno Kessler, 18 Via Sommarive, 38055 Povo (Trento), Italy.
25. Ashok K. Chandra, Dexter C. Kozen & Larry J. Stockmeyer (1981): Alternation. JACM 28(1), pp. 114–133, doi:10.1145/322234.322243.
26. Frank Ciesinski, Christel Baier, Marcus Größer & David Parker (2008): Generating compact MTBDD-representations from Probmela specifications. In: SPIN, pp. 60–76, doi:10.1007/978-3-540-85114-1_7.
27. Edsger W. Dijkstra (1975): Guarded commands, nondeterminacy and formal derivation of programs. CACM 18(8), pp. 453–457, doi:10.1145/360933.360975.
28. M.B. Dwyer, G.S. Avrunin & J.C. Corbett (1999): Patterns in property specifications for finite-state verification. In: ICSE, pp. 411–420, doi:10.1145/302405.302672.
29. Rüdiger Ehlers (2011): Experimental aspects of synthesis. EPTCS 50, doi:10.4204/EPTCS.50.
30. Rüdiger Ehlers (2011): Generalized Rabin(1) synthesis with applications to robust system synthesis. In: NFM, pp. 101–115, doi:10.1007/978-3-642-20398-5_9.
31. Rüdiger Ehlers (2011): Unbeast: Symbolic bounded synthesis. In: TACAS, pp. 272–275, doi:10.1007/978-3-642-19835-9_25.
32. Rüdiger Ehlers & Vasumathi Raman (2014): Low-effort specification debugging and analysis. EPTCS 157, pp. 117–133, doi:10.4204/EPTCS.157.12.
33. Ioannis Filippidis & contributors (2013): List of verification and synthesis tools. Available at https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md.
34. Ioannis Filippidis & Richard M. Murray (2015): Revisiting the AMBA AHB bus case study. Technical Report CaltechCDSTR:2015.004. California Institute of Technology, Pasadena, CA. Available at http://resolver.caltech.edu/CaltechCDSTR:2015.004.
35. Ioannis Filippidis, Richard M. Murray & Gerard J. Holzmann (2015): Synthesis from multi-paradigm specifications. Technical Report CaltechCDSTR:2015.003. California Institute of Technology, Pasadena, CA. Available at http://resolver.caltech.edu/CaltechCDSTR:2015.003.
36. Bernd Finkbeiner & Sven Schewe (2013): Bounded synthesis. International Journal on Software Tools for Technology Transfer (STTT) 15(5-6), pp. 519–539, doi:10.1007/s10009-012-0228-z.
37. Robert W. Floyd (1967): Nondeterministic algorithms. JACM 14(4), pp. 636–644, doi:10.1145/321420.321422.
38. Bjorn N. Freeman-Benson (1990): Kaleidoscope: Mixing objects, constraints, and imperative programming. In: OOPSLA/ECOOP, pp. 77–88, doi:10.1145/97946.97957.
39. Bjørn N. Freeman-Benson & Alan Borning (1992): Integrating constraints with an object-oriented language. In: ECOOP, pp. 268–286, doi:10.1007/BFb0053042.
40. B.N. Freeman-Benson & A Borning (1992): The design and implementation of Kaleidoscope'90-A constraint imperative programming language. In: ICCL, pp. 174–180, doi:10.1109/ICCL.1992.185480.
41. Abdoulaye Gamatié (2010): Designing embedded systems with the Signal programming language: synchronous, reactive specification. Springer, doi:10.1007/978-1-4419-0941-1.
42. Jeff Gennari, Shaun Hedrick, Fred Long, Justin Pincar & Robert Seacord (2007): Ranged integers for the C programming language. Technical Note CMU/SEI-2007-TN-027. Software Engineering Institute, Carnegie Mellon University. Available at http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=8265.
43. Yashdeep Godhal, Krishnendu Chatterjee & Thomas A Henzinger (2013): Synthesis of AMBA AHB from formal specification: a case study. International Journal on Software Tools for Technology Transfer (STTT) 15(5-6), pp. 585–601, doi:10.1007/s10009-011-0207-9.
44. Nicolas Halbwachs (1993): Synchronous programming of reactive systems. Engineering and Computer Science 215. Springer, doi:10.1007/978-1-4757-2231-4. Available at http://www-verimag.imag.fr/~halbwach/newbook.pdf.
45. Charles Antony Richard Hoare (1985, 2004): Communicating sequential processes 178. Prentice-Hall. Available at http://www.usingcsp.com/cspbook.pdf.
46. Gerard J. Holzmann: Promela Language Reference (http://spinroot.com/spin/Man/promela.html). Available at http://spinroot.com/spin/Man/promela.html.
47. Gerard J. Holzmann (2003): The SPIN model checker: Primer and reference manual. Addison-Wesley.
48. Yong Jiang & Zongyan Qiu (2012): S2N: model transformation from Spin to NuSMV. In: SPIN, pp. 255–260, doi:10.1007/978-3-642-31759-0_20.
49. Barbara Jobstmann & Roderick Bloem (2006): Optimizations for LTL synthesis. In: FMCAD, pp. 117–124, doi:10.1109/FMCAD.2006.22.
50. Barbara Jobstmann, Stefan Galler, Martin Weiglhofer & Roderick Bloem (2007): Anzu: A tool for property synthesis. In: CAV, pp. 258–262, doi:10.1007/978-3-540-73368-3_29.
51. Barbara Jobstmann, Andreas Griesmayer & Roderick Bloem (2005): Program repair as a game. In: CAV, pp. 226–238, doi:10.1007/11513988_23.
52. Muriel Jourdan, Fabienne Lagnier, R Maraninchi & Pascal Raymond (1994): A multiparadigm language for reactive systems. In: ICCL, pp. 211–218, doi:10.1109/ICCL.1994.288379.
53. Robert M. Keller (1976): Formal verification of parallel programs. CACM 19(7), pp. 371–384, doi:10.1145/360248.360251.
54. Yonit Kesten, Amir Pnueli & Li-on Raviv (1998): Algorithmic verification of linear temporal logic specifications. In: ICALP 1443, pp. 1–16, doi:10.1007/BFb0055036.
55. Uri Klein, Nir Piterman & Amir Pnueli (2012): Effective synthesis of asynchronous systems from GR(1) specifications. In: VMCAI, pp. 283–298, doi:10.1007/978-3-642-27940-9_19.
56. M. Kloetzer & C. Belta (2008): A fully automated framework for control of linear systems from temporal logic specifications. TAC 53(1), pp. 287–297, doi:10.1109/TAC.2007.914952.
57. H. Kress-Gazit, G.E. Fainekos & G.J. Pappas (2009): Temporal-logic-based reactive mission and motion planning. IEEE Transactions on Robotics (TRO) 25(6), pp. 1370–1381, doi:10.1109/TRO.2009.2030225.
58. Daniel Kroening & Ofer Strichman (2008): Decision procedures: An algorithmic point of view. Springer.
59. O. Kupferman & M.Y. Vardi (2005): Safraless decision procedures. In: FOCS, pp. 531–540, doi:10.1109/SFCS.2005.66.
60. Orna Kupferman (2012): Recent challenges and ideas in temporal synthesis. In: SOFSEM, pp. 88–98, doi:10.1007/978-3-642-27660-6_8.
61. Leslie Lamport (1994): The Temporal Logic of Actions. ACM Trans. Program. Lang. Syst. 16(3), pp. 872–923, doi:10.1145/177492.177726.
62. Leslie Lamport (2002): Specifying systems: The TLA+ language and tools or hardware and software engineers. Addison-Wesley. Available at http://research.microsoft.com/en-us/um/people/lamport/tla/book.html.
63. Leslie Lamport & Fred B. Schneider (1985): Constraints: A uniform approach to aliasing and typing. In: POPL, pp. 205–216, doi:10.1145/318593.318640.
64. K Rustan M Leino (2010): Dafny: An automatic program verifier for functional correctness. In: LPAR 6355, pp. 348–370, doi:10.1007/978-3-642-17511-4_20.
65. A Solar Lezama (2008): Program synthesis by sketching. Citeseer. Available at http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-177.html.
66. Orna Lichtenstein, Amir Pnueli & Lenore Zuck (1985): The glory of the past. In: Logics of Programs 193, pp. 196–218, doi:10.1007/3-540-15648-8_16.
67. Scott C. Livingston, Richard M. Murray & Joel W. Burdick (2012): Backtracking temporal logic synthesis for uncertain environments. In: ICRA, pp. 5163–5170, doi:10.1109/ICRA.2012.6225208.
68. Gus Lopez, Bjorn Freeman-Benson & Alan Borning (1994): Implementing constraint imperative programming languages: The Kaleidoscope'93 virtual machine. In: OOPSLA, pp. 259–271, doi:10.1145/191080.191118.
69. Z Manna & Amir Pnueli (1990): Tools and rules for the practicing verifier. Technical Report CS-TR-90-1321. Stanford University, CA, USA. Available at http://i.stanford.edu/pub/cstr/reports/cs/tr/90/1321/CS-TR-90-1321.pdf.
70. Zohar Manna & Amir Pnueli (1989): The anchored version of the temporal framework. In: Linear time, branching time and partial order in Logics and models for concurrency, LNCS 354. Springer, pp. 201–284, doi:10.1007/BFb0013024.
71. Zohar Manna & Amir Pnueli (1990): A hierarchy of temporal properties. In: PODC, pp. 377–410, doi:10.1145/93385.93442.
72. Shahar Maoz & Yaniv Sa'ar (2011): AspectLTL: An aspect language for LTL specifications. In: Aspect-oriented Software Development (AOSD). ACM, pp. 19–30, doi:10.1145/1960275.1960280.
73. John McCarthy (1959): A basis for a mathematical theory of computation. In: P. Braffort & D. Hirschberg: Computer Programming and Formal Systems, Studies in Logic and the Foundations of Mathematics 26. North-Holland, pp. 33–70, doi:10.1016/S0049-237X(09)70099-0.
74. Kenneth Lauchlin McMillan (1992): Symbolic model checking: An approach to the state explosion problem. Carnegie Mellon University, Pittsburgh, PA, USA, doi:10.1007/978-1-4615-3190-6. Available at http://www.kenmcmil.com/pubs/thesis.pdf. UMI Order No. GAX92-24209.
75. George H Mealy (1955): A method for synthesizing sequential circuits. Bell System Technical Journal 34(5), pp. 1045–1079, doi:10.1002/j.1538-7305.1955.tb03788.x.
76. Edward F Moore (1956): Gedanken-experiments on sequential machines. Automata studies 34, pp. 129–153.
77. A. Morgenstern (2010): Symbolic controller synthesis for LTL specifications. Computer Science. Available at http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:hbz:386-kluedo-25721.
78. A. Morgenstern & K. Schneider (2011): A LTL fragment for GR(1)-synthesis. EPTCS 50, pp. 33–45, doi:10.4204/EPTCS.50.3.
79. David E Muller, Ahmed Saoudi & Paul E Schupp (1986): Alternating automata, the weak monadic theory of the tree, and its complexity. In: ICALP, pp. 275–283, doi:10.1007/3-540-16761-7_77.
80. Elie Najm & Frank Olsen (1996): Protocol verification with Reactive Proela/RSPIN. In: SPIN, pp. 109–128. Available at http://spinroot.com/spin/Workshops/ws96/Ol.pdf.
81. Elie Najm & Frank Olsen (1996): Reactive EFSMs — Reactive Promela/RSPIN. In: TACAS, pp. 349–368, doi:10.1007/3-540-61042-1_54.
82. Shipra Panda & Fabio Somenzi (1995): Who are the variables in your neighbourhood. In: ICCAD, pp. 74–77, doi:10.1109/ICCAD.1995.479994.
83. Nir Piterman, Amir Pnueli & Yaniv Sa'ar (2006): Synthesis of reactive(1) designs. In: VMCAI, pp. 364–380, doi:10.1007/11609773_24.
84. A. Pnueli & R. Rosner (1989): On the synthesis of a reactive module. In: POPL, pp. 179–190, doi:10.1145/75277.75293.
85. Amir Pnueli (1977): The temporal logic of programs. In: FOCS, pp. 46 –57, doi:10.1109/SFCS.1977.32.
86. Amir Pnueli & Uri Klein (2009): Synthesis of programs from temporal property specifications. In: MEMOCODE, pp. 1–7, doi:10.1109/MEMCOD.2009.5185372.
87. Amir Pnueli & Roni Rosner (1989): On the synthesis of an asynchronous reactive module. In: ICALP, pp. 652–671, doi:10.1007/BFb0035790.
88. Amir Pnueli, Yaniv Sa'ar & Lenore D Zuck (2010): Jtlv: A framework for developing verification algorithms. In: CAV, pp. 171–174, doi:10.1007/978-3-642-14295-6_18.
89. Roni Rosner (1992): Modular synthesis of reactive systems. Weizmann Institute of Science, Rehovot, Israel. Available at http://www.researchgate.net/publication/238759536_Modular_synthesis_of_reactive_systems/file/50463527f8b648c3ba.pdf.
90. Richard Rudell (1993): Dynamic variable ordering for ordered binary decision diagrams. In: ICCAD, pp. 42–47, doi:10.1109/ICCAD.1993.580029.
91. Matthias Schlaipfer, Georg Hofferek & Roderick Bloem (2012): Generalized reactivity(1) synthesis without a monolithic strategy. In: HSVT, pp. 20–34, doi:10.1007/978-3-642-34188-5_6.
92. Klaus Schneider (2004): Verification of reactive systems: formal methods and algorithms. Springer, doi:10.1007/978-3-662-10778-2.
93. Saqib Sohail, Fabio Somenzi & Kavita Ravi (2008): A hybrid algorithm for LTL games. In: VMCAI, pp. 309–323, doi:10.1007/978-3-540-78163-9_26.
94. Fabio Somenzi (2012): Cudd: CU Decision Diagram package - release 2.5.0. University of Colorado at Boulder. Available at http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html.
95. Harald Søndergaard & Peter Sestoft (1992): Non-determinism in functional languages. The Computer Journal 35(5), pp. 514–523, doi:10.1093/comjnl/35.5.514.
96. Wolfgang Thomas (2008): Solution of Church's Problem: A tutorial. New Perspectives on Games and interaction 5.
97. Peter Van-Roy & Seif Haridi (2004): Concepts, techniques, and models of computer programming. MIT press.
98. Moshe Y Vardi (1995): Alternating automata and program verification. In: Computer Science Today. Springer, pp. 471–485, doi:10.1007/BFb0015261.
99. Moshe Y Vardi (1996): An automata-theoretic approach to linear temporal logic. In: Logics for concurrency, LNCS 1043. Springer, pp. 238–266, doi:10.1007/3-540-60915-6_6.
100. Igor Walukiewicz (2004): A Landscape with games in the background. LICS 0, pp. 356–366, doi:10.1109/LICS.2004.1319630.
101. Tichakorn Wongpiromsarn, Ufuk Topcu & Richard M Murray (2013): Synthesis of control protocols for autonomous systems. Unmanned Systems 1(01), pp. 21–39, doi:10.1142/S2301385013500027.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org