@inproceedings(AminofJKR14,
 author       = "Benjamin Aminof and Swen Jacobs and Ayrat Khalimov and Sasha Rubin",
 year         = "2014",
 title        = "Parameterized Model Checking of Token-Passing Systems",
 booktitle    = "VMCAI",
 series       = "LNCS",
 volume       = "8318",
 publisher    = "Springer",
 pages        = "262--281",
 doi          = "10.1007/978-3-642-54013-4\_15",
)
@misc(AMBASpec,
 author       = "{ARM Ltd.}",
 year         = "1999",
 title        = "{AMBA} Specification (Rev.2)",
 howpublished = "Available from www.arm.com",
)
@inproceedings(ltl3ba,
 author       = "Tom{\'a}s Babiak and Mojm\'{\i }r Kret\'{\i }nsk{\'y} and Vojtech Reh{\'a}k and Jan Strejcek",
 year         = "2012",
 title        = "LTL to B{\"u}chi Automata Translation: Fast and More Deterministic",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "7214",
 publisher    = "Springer",
 pages        = "95--109",
 doi          = "10.1007/978-3-642-28756-5\_8",
)
@inproceedings(Bloem10c,
 author       = "Roderick Bloem and Alessandro Cimatti and Karin Greimel and Georg Hofferek and Robert K{\"o}nighofer and Marco Roveri and Viktor Schuppan and Richard Seeber",
 year         = "2010",
 title        = "RATSY - A New Requirements Analysis Tool with Synthesis",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "6174",
 publisher    = "Springer",
 pages        = "425--429",
 doi          = "10.1007/978-3-642-14295-6\_37",
)
@article(full-version,
 author       = "Roderick Bloem and Swen Jacobs and Ayrat Khalimov",
 year         = "2014",
 title        = "Parameterized Synthesis Case Study: AMBA AHB (Extended Version)",
 journal      = "arXiv:1406.7608",
 url          = "http://arxiv.org/abs/1406.7608",
)
@article(Bloem12,
 author       = "Roderick Bloem and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Yaniv Sa'ar",
 year         = "2012",
 title        = "Synthesis of Reactive(1) designs",
 journal      = "J. Comput. Syst. Sci.",
 volume       = "78",
 number       = "3",
 pages        = "911--938",
 doi          = "10.1016/j.jcss.2011.08.007",
)
@article(Emerso03,
 author       = "E. Allen Emerson and Kedar S. Namjoshi",
 year         = "2003",
 title        = "On Reasoning About Rings",
 journal      = "Int. J. Found. Comput. Sci.",
 volume       = "14",
 number       = "4",
 pages        = "527--550",
 doi          = "10.1142/S0129054103001881",
)
@inproceedings(Finkbeiner12,
 author       = "Bernd Finkbeiner and Swen Jacobs",
 year         = "2012",
 title        = "Lazy Synthesis",
 booktitle    = "VMCAI",
 series       = "LNCS",
 volume       = "7148",
 publisher    = "Springer",
 pages        = "219--234",
 doi          = "10.1007/978-3-642-27940-9\_15",
)
@article(Finkbeiner13,
 author       = "Bernd Finkbeiner and Sven Schewe",
 year         = "2013",
 title        = "Bounded synthesis",
 journal      = "STTT",
 volume       = "15",
 number       = "5-6",
 pages        = "519--539",
 doi          = "10.1007/s10009-012-0228-z",
)
@article(GodhalCH13,
 author       = "Yashdeep Godhal and Krishnendu Chatterjee and Thomas A. Henzinger",
 year         = "2013",
 title        = "Synthesis of AMBA AHB from formal specification: a case study",
 journal      = "STTT",
 volume       = "15",
 number       = "5-6",
 pages        = "585--601",
 doi          = "10.1007/s10009-011-0207-9",
)
@article(Jacobs14,
 author       = "Swen Jacobs and Roderick Bloem",
 year         = "2014",
 title        = "Parameterized Synthesis",
 journal      = "Logical Methods in Computer Science",
 volume       = "10",
 pages        = "1--29",
 doi          = "10.2168/LMCS-10(1:12)2014",
)
@phdthesis(BarbaraThesis,
 author       = "Barbara Jobstmann",
 year         = "2007",
 title        = "Applications and Optimizations for LTL Synthesis",
 school       = "Graz University of Technology",
)
@inproceedings(Party,
 author       = "Ayrat Khalimov and Swen Jacobs and Roderick Bloem",
 year         = "2013",
 title        = "PARTY Parameterized Synthesis of Token Rings",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "8044",
 publisher    = "Springer",
 pages        = "928--933",
 doi          = "10.1007/978-3-642-39799-8\_66",
)
@inproceedings(TEPS,
 author       = "Ayrat Khalimov and Swen Jacobs and Roderick Bloem",
 year         = "2013",
 title        = "Towards Efficient Parameterized Synthesis",
 booktitle    = "VMCAI",
 series       = "LNCS",
 volume       = "7737",
 publisher    = "Springer",
 pages        = "108--127",
 doi          = "10.1007/978-3-642-35873-9\_9",
)
@inproceedings(Klein10,
 author       = "Uri Klein and Amir Pnueli",
 year         = "2010",
 title        = "Revisiting Synthesis of GR(1) Specifications",
 booktitle    = "Haifa Verification Conference",
 series       = "LNCS",
 volume       = "6504",
 publisher    = "Springer",
 pages        = "161--181",
 doi          = "10.1007/978-3-642-19583-9\_16",
)
@inproceedings(Moura08,
 author       = "Leonardo de Moura and Nikolaj Bj{\o }rner",
 year         = "2008",
 title        = "Z3: An Efficient {SMT} Solver",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "4963",
 publisher    = "Springer",
 pages        = "337--340",
 doi          = "10.1007/978-3-540-78800-3\_24",
)
@inproceedings(Pnueli90,
 author       = "Amir Pnueli and Roni Rosner",
 year         = "1990",
 title        = "Distributed Reactive Systems Are Hard to Synthesize",
 booktitle    = "FOCS",
 publisher    = "IEEE Computer Society",
 pages        = "746--757",
 doi          = "10.1109/FSCS.1990.89597",
)