@inproceedings(DBLP:conf/icalp/AbadiLW89,
 author       = "Mart\'{\i }n Abadi and Leslie Lamport and Pierre Wolper",
 year         = "1989",
 title        = "Realizable and Unrealizable Specifications of Reactive Systems",
 editor       = "\write \rebib { editor = "Ausiello",}",
 pages        = "1--17",
 doi          = "10.1007/BFb0035748",
)
@misc(AMBA1999,
 author       = "{ARM Ltd.}",
 year         = "1999",
 title        = "AMBA{\texttrademark } specification (rev. 2)",
 howpublished = "Available at \burl {www.arm.com}",
)
@proceedings(DBLP:conf/icalp/1989,
 editor       = "Giorgio Ausiello and Mariangiola Dezani-Ciancaglini and Simona Ronchi Della Rocca",
 year         = "1989",
 title        = "Automata, Languages and Programming, 16th International Colloquium, (ICALP)",
 series       = "LNCS",
 volume       = "372",
 publisher    = "Springer",
)
@book(Biere2009,
 editor       = "Armin Biere and Marijn Heule and Hans van Maaren and Toby Walsh",
 year         = "2009",
 title        = "Handbook of Satisfiability",
 publisher    = "IOS Press",
)
@inproceedings(DBLP:conf/cav/BloemCGHJ10,
 author       = "Roderick Bloem and Krishnendu Chatterjee and Karin Greimel and Thomas A. Henzinger and Barbara Jobstmann",
 year         = "2010",
 title        = "Robustness in the Presence of Liveness",
 editor       = "\write \rebib { editor = "Touili",}",
 pages        = "410--424",
 doi          = "10.1007/978-3-642-14295-6_36",
)
@inproceedings(DBLP:conf/cav/BloemCGHKRSS10,
 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",
 editor       = "\write \rebib { editor = "Touili",}",
 pages        = "425--429",
 doi          = "10.1007/978-3-642-14295-6_37",
)
@inproceedings(DBLP:conf/date/BloemGJPPW07,
 author       = "Roderick Bloem and Stefan Galler and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Martin Weiglhofer",
 year         = "2007",
 title        = "Interactive presentation: Automatic hardware synthesis from specifications: a case study",
 editor       = "Rudy Lauwereins and Jan Madsen",
 booktitle    = "DATE",
 publisher    = "ACM",
 pages        = "1188--1193",
 doi          = "10.1145/1266366.1266622",
)
@article(DBLP:journals/entcs/BloemGJPPW07,
 author       = "Roderick Bloem and Stefan Galler and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Martin Weiglhofer",
 year         = "2007",
 title        = "Specify, Compile, Run: Hardware from PSL",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "190",
 number       = "4",
 pages        = "3--16",
 doi          = "10.1016/j.entcs.2007.09.004",
)
@misc(AnzuTool,
 author       = "Roderick Bloem and Barbara Jobstmann and Martin Weiglhofer",
 year         = "2007",
 title        = "Anzu",
 howpublished = "\burl {http://www.ist.tugraz.at/staff/jobstmann/anzu/}",
)
@article(DBLP:journals/tc/Bryant86,
 author       = "Randal E. Bryant",
 year         = "1986",
 title        = "Graph-Based Algorithms for Boolean Function Manipulation",
 journal      = "IEEE Trans. Computers",
 volume       = "35",
 number       = "8",
 pages        = "677--691",
)
@inproceedings(DBLP:conf/concur/CassezDFLL05,
 author       = "Franck Cassez and Alexandre David and Emmanuel Fleury and Kim Guldstrand Larsen and Didier Lime",
 year         = "2005",
 title        = "Efficient On-the-Fly Algorithms for the Analysis of Timed Games",
 editor       = "Mart\'{\i }n Abadi and Luca de Alfaro",
 booktitle    = "CONCUR",
 series       = "LNCS",
 volume       = "3653",
 publisher    = "Springer",
 pages        = "66--80",
 doi          = "10.1007/11539452_9",
)
@inproceedings(DBLP:conf/concur/ClementeM10,
 author       = "Lorenzo Clemente and Richard Mayr",
 year         = "2010",
 title        = "Multipebble Simulations for Alternating Automata - (Extended Abstract)",
 editor       = "Paul Gastin and Fran\c {c}ois Laroussinie",
 booktitle    = "CONCUR",
 series       = "LNCS",
 volume       = "6269",
 publisher    = "Springer",
 pages        = "297--312",
 doi          = "10.1007/978-3-642-15375-4_21",
)
@misc(AcaciaTool,
 author       = "Laurent Doyen and Emmanuel Filiot and Naiyong Jin and Jean-Fran{\c {c}}ois Raskin",
 year         = "2009",
 title        = "Acacia - LTL Realizability Check and Winning Strategy Synthesis using Antichains",
 howpublished = "\burl {http://www.antichains.be/acacia/}",
)
@inproceedings(DBLP:conf/mascots/Duret-LutzP04,
 author       = "Alexandre Duret-Lutz and Denis Poitrenaud",
 year         = "2004",
 title        = "SPOT: An Extensible Model Checking Library Using Transition-Based Generalized B{\"u}chi Automata",
 editor       = "Doug DeGroot and Peter G. Harrison and Harry A. G. Wijshoff and Zary Segall",
 booktitle    = "MASCOTS",
 publisher    = "IEEE Computer Society",
 pages        = "76--83",
)
@inproceedings(DBLP:conf/sat/Ehlers10,
 author       = "R{\"u}diger Ehlers",
 year         = "2010",
 title        = "Minimising Deterministic B{\"u}chi Automata Precisely Using SAT Solving",
 editor       = "Strichman and Szeider",
 pages        = "326--332",
 doi          = "10.1007/978-3-642-14186-7_28",
)
@inproceedings(DBLP:conf/cav/Ehlers10,
 author       = "R{\"u}diger Ehlers",
 year         = "2010",
 title        = "Symbolic Bounded Synthesis",
 editor       = "\write \rebib { editor = "Touili",}",
 pages        = "365--379",
 doi          = "10.1007/978-3-642-14295-6_33",
)
@misc(UnbeastTool,
 author       = "R{\"u}diger Ehlers",
 year         = "2010",
 title        = "Unbeast {--} Symbolic Bounded Synthesis",
 howpublished = "\burl {http://react.cs.uni-saarland.de/tools/unbeast/}",
)
@inproceedings(DBLP:conf/spin/EhlersF10,
 author       = "R{\"u}diger Ehlers and Bernd Finkbeiner",
 year         = "2010",
 title        = "On the Virtue of Patience: Minimizing B{\"u}chi Automata",
 editor       = "van de Pol and Weber",
 pages        = "129--145",
 doi          = "10.1007/978-3-642-16164-3_10",
)
@book(PSLBook,
 author       = "Cindy Eisner and Dana Fisman",
 year         = "2006",
 title        = "A Practical Introduction to PSL (Series on Integrated Circuits and Systems)",
 publisher    = "Springer-Verlag",
)
@proceedings(DBLP:conf/cav/2000,
 editor       = "E. Allen Emerson and A. Prasad Sistla",
 year         = "2000",
 title        = "Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings",
 series       = "LNCS",
 volume       = "1855",
 publisher    = "Springer",
)
@article(DBLP:journals/heuristics/Falkenauer98,
 author       = "Emanuel Falkenauer",
 year         = "1998",
 title        = "On Method Overfitting",
 journal      = "J. Heuristics",
 volume       = "4",
 number       = "3",
 pages        = "281--287",
)
@inproceedings(DBLP:conf/cav/FiliotJR09,
 author       = "Emmanuel Filiot and Naiyong Jin and Jean-Fran\c {c}ois Raskin",
 year         = "2009",
 title        = "An Antichain Algorithm for {LTL} Realizability",
 editor       = "Ahmed Bouajjani and Oded Maler",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "5643",
 publisher    = "Springer",
 pages        = "263--277",
 doi          = "10.1007/978-3-642-02658-4_22",
)
@inproceedings(DBLP:conf/atva/FiliotJR10,
 author       = "Emmanuel Filiot and Naiyong Jin and Jean-Fran\c {c}ois Raskin",
 year         = "2010",
 title        = "Compositional Algorithms for {LTL} Synthesis",
 editor       = "Ahmed Bouajjani and Wei-Ngan Chin",
 booktitle    = "ATVA",
 series       = "LNCS",
 volume       = "6252",
 publisher    = "Springer",
 pages        = "112--127",
 doi          = "10.1007/978-3-642-15643-4_10",
)
@inproceedings(DBLP:conf/lics/FinkbeinerS05,
 author       = "Bernd Finkbeiner and Sven Schewe",
 year         = "2005",
 title        = "Uniform Distributed Synthesis",
 booktitle    = "LICS",
 publisher    = "IEEE Computer Society",
 pages        = "321--330",
 doi          = "10.1109/LICS.2005.53",
)
@article(DBLP:journals/jcss/FischerL79,
 author       = "Michael J. Fischer and Richard E. Ladner",
 year         = "1979",
 title        = "Propositional Dynamic Logic of Regular Programs",
 journal      = "J. Comput. Syst. Sci.",
 volume       = "18",
 number       = "2",
 pages        = "194--211",
)
@inproceedings(DBLP:conf/aspdac/ForthM00,
 author       = "Riccardo Forth and Paul Molitor",
 year         = "2000",
 title        = "An efficient heuristic for state encoding minimizing the BDD representations of the transistion relations of finite state machines",
 booktitle    = "ASP-DAC",
 publisher    = "ACM",
 pages        = "61--66",
)
@inproceedings(DBLP:conf/cav/GastinO01,
 author       = "Paul Gastin and Denis Oddoux",
 year         = "2001",
 title        = "Fast {LTL} to {B}{\"u}chi Automata Translation",
 editor       = "G{\'e}rard Berry and Hubert Comon and Alain Finkel",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "2102",
 publisher    = "Springer",
 pages        = "53--65",
)
@proceedings(POS2010,
 editor       = "Allen Van Gelder and Daniel Le Berre",
 year         = "2010",
 title        = "Pragmatics of SAT",
 address      = "Workshop at the Federated Logic Conference (FLoC) 2010, Edinburgh",
)
@inproceedings(DBLP:conf/spin/GhafariHR10,
 author       = "Naghmeh Ghafari and Alan J. Hu and Zvonimir Rakamaric",
 year         = "2010",
 title        = "Context-Bounded Translations for Concurrent Software: An Empirical Evaluation",
 editor       = "van de Pol and Weber",
 pages        = "227--244",
 doi          = "10.1007/978-3-642-16164-3_17",
)
@article(DBLP:journals/corr/abs-1001-2811,
 author       = "Yashdeep Godhal and Krishnendu Chatterjee and Thomas A. Henzinger",
 year         = "2010",
 title        = "Synthesis of AMBA AHB from Formal Specification",
 journal      = "CoRR",
 volume       = "abs/1001.2811",
 url          = "http://arxiv.org/abs/1001.2811",
)
@article(DBLP:journals/amcs/GostiVSS07,
 author       = "Wilsin Gosti and Tiziano Villa and Alexander Saldanha and Alberto L. Sangiovanni-Vincentelli",
 year         = "2007",
 title        = "FSM Encoding for BDD Representations",
 journal      = "Applied Mathematics and Computer Science",
 volume       = "17",
 number       = "1",
 pages        = "113--124",
 doi          = "10.2478/v10006-007-0011-6",
)
@proceedings(DBLP:conf/dagstuhl/2001automata,
 editor       = "Erich Gr{\"a}del and Wolfgang Thomas and Thomas Wilke",
 year         = "2002",
 title        = "Automata, Logics, and Infinite Games: A Guide to Current Research",
 series       = "LNCS",
 volume       = "2500",
 publisher    = "Springer",
)
@inproceedings(DBLP:conf/icalp/GreimelBJV08,
 author       = "Karin Greimel and Roderick Bloem and Barbara Jobstmann and Moshe Y. Vardi",
 year         = "2008",
 title        = "Open Implication",
 editor       = "Luca Aceto and Ivan Damg{\r a}rd and Leslie Ann Goldberg and Magn{\'u}s M. Halld{\'o}rsson and Anna Ing{\'o}lfsd{\'o}ttir and Igor Walukiewicz",
 booktitle    = "ICALP (2)",
 series       = "LNCS",
 volume       = "5126",
 publisher    = "Springer",
 pages        = "361--372",
 doi          = "10.1007/978-3-540-70583-3_30",
)
@inproceedings(DBLP:conf/tacas/HardingRS05,
 author       = "Aidan Harding and Mark Ryan and Pierre-Yves Schobbens",
 year         = "2005",
 title        = "A New Algorithm for Strategy Synthesis in {LTL} Games",
 editor       = "Nicolas Halbwachs and Lenore D. Zuck",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "3440",
 publisher    = "Springer",
 pages        = "477--492",
)
@inproceedings(DBLP:conf/csl/HenzingerP06,
 author       = "Thomas A. Henzinger and Nir Piterman",
 year         = "2006",
 title        = "Solving Games Without Determinization",
 editor       = "Zolt{\'a}n {\'E}sik",
 booktitle    = "CSL",
 series       = "LNCS",
 volume       = "4207",
 publisher    = "Springer",
 pages        = "395--410",
 doi          = "10.1007/11874683_26",
)
@misc(IBMTutorial,
 author       = "{IBM R}esearch",
 title        = "RuleBase formal verification tool tutorial",
 howpublished = "\burl {https://www.research.ibm.com/haifa/projects/verification/RB_Homepage/}",
)
@misc(LilyTool,
 author       = "Barbara Jobstmann and Roderick Bloem",
 year         = "2006",
 title        = "Lily - a LInear Logic sYnthesizer",
 howpublished = "\burl {http://www.iaik.tugraz.at/content/research/design_verification/lily/}",
)
@inproceedings(DBLP:conf/fmcad/JobstmannB06,
 author       = "Barbara Jobstmann and Roderick Bloem",
 year         = "2006",
 title        = "Optimizations for {LTL} Synthesis",
 booktitle    = "FMCAD",
 publisher    = "IEEE Computer Society",
 pages        = "117--124",
 doi          = "10.1109/FMCAD.2006.22",
)
@inproceedings(DBLP:conf/cav/JobstmannGWB07,
 author       = "Barbara Jobstmann and Stefan Galler and Martin Weiglhofer and Roderick Bloem",
 year         = "2007",
 title        = "Anzu: A Tool for Property Synthesis",
 editor       = "Werner Damm and Holger Hermanns",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "4590",
 publisher    = "Springer",
 pages        = "258--262",
 doi          = "10.1007/978-3-540-73368-3_29",
)
@article(DBLP:journals/tcs/KleinB06,
 author       = "Joachim Klein and Christel Baier",
 year         = "2006",
 title        = "Experiments with deterministic {$\omega $}-automata for formulas of linear temporal logic",
 journal      = "Theor. Comput. Sci.",
 volume       = "363",
 number       = "2",
 pages        = "182--195",
 doi          = "10.1016/j.tcs.2006.07.022",
)
@inproceedings(Klein2010,
 author       = "Uri Klein and Amir Pnueli",
 year         = "2010",
 title        = "Revisiting Synthesis of {GR(1)} Specifications",
 booktitle    = "HVC",
 series       = "LNCS",
 volume       = "6504",
)
@inproceedings(DBLP:conf/sat/Kottler10,
 author       = "Stephan Kottler",
 year         = "2010",
 title        = "SAT Solving with Reference Points",
 editor       = "Strichman and Szeider",
 pages        = "143--157",
 doi          = "10.1007/978-3-642-14186-7_13",
)
@inproceedings(DBLP:conf/cav/KukulaS00,
 author       = "James H. Kukula and Thomas R. Shiple",
 year         = "2000",
 title        = "Building Circuits from Relations",
 editor       = "Emerson and Sistla",
 pages        = "113--123",
)
@inproceedings(DBLP:conf/lics/Kupferman06,
 author       = "Orna Kupferman",
 year         = "2006",
 title        = "Avoiding Determinization",
 booktitle    = "LICS",
 publisher    = "IEEE Computer Society",
 pages        = "243--254",
 doi          = "10.1109/LICS.2006.15",
)
@inproceedings(DBLP:conf/cav/KupfermanPV06,
 author       = "Orna Kupferman and Nir Piterman and Moshe Y. Vardi",
 year         = "2006",
 title        = "Safraless Compositional Synthesis",
 editor       = "Thomas Ball and Robert B. Jones",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "4144",
 publisher    = "Springer",
 pages        = "31--44",
 doi          = "10.1007/11817963_6",
)
@article(DBLP:journals/bsl/KupfermanV99,
 author       = "Orna Kupferman and Moshe Y. Vardi",
 year         = "1999",
 title        = "Church's problem revisited",
 journal      = "Bulletin of Symbolic Logic",
 volume       = "5",
 number       = "2",
 pages        = "245--263",
 url          = "http://www.math.ucla.edu/~asl/bsl/0502/0502-004.ps",
)
@article(DBLP:journals/fmsd/KupfermanV01,
 author       = "Orna Kupferman and Moshe Y. Vardi",
 year         = "2001",
 title        = "Model Checking of Safety Properties",
 journal      = "Formal Methods in System Design",
 volume       = "19",
 number       = "3",
 pages        = "291--314",
)
@inproceedings(DBLP:conf/lics/KupfermanV01,
 author       = "Orna Kupferman and Moshe Y. Vardi",
 year         = "2001",
 title        = "Synthesizing Distributed Systems",
 booktitle    = "LICS",
)
@inproceedings(DBLP:conf/focs/KupfermanV05,
 author       = "Orna Kupferman and Moshe Y. Vardi",
 year         = "2005",
 title        = "Safraless Decision Procedures",
 booktitle    = "FOCS",
 publisher    = "IEEE",
 pages        = "531--542",
 doi          = "10.1109/SFCS.2005.66",
)
@inproceedings(DBLP:conf/icalp/LiuS98,
 author       = "Xinxin Liu and Scott A. Smolka",
 year         = "1998",
 title        = "Simple Linear-Time Algorithms for Minimal Fixed Points (Extended Abstract)",
 editor       = "Kim G. Larsen and Sven Skyum and Glynn Winskel",
 booktitle    = "ICALP",
 series       = "LNCS",
 volume       = "1443",
 publisher    = "Springer",
 pages        = "53--66",
 doi          = "10.1007/978-3-540-64781-2_53",
)
@phdthesis(Morg10,
 author       = "A. Morgenstern",
 year         = "2010",
 title        = "Symbolic Controller Synthesis for {LTL} Specifications",
 school       = "Department of Computer Science, University of Kaiserslautern, Germany",
)
@inproceedings(DBLP:journals/corr/abs-1006-1408,
 author       = "A. Morgenstern and K. Schneider",
 year         = "2010",
 title        = "Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient {LTL} Synthesis",
 editor       = "A. Montanari and M. Napoli and M. Parente",
 booktitle    = "{GandALF}",
 series       = "EPTCS",
 volume       = "25",
 pages        = "89--102",
 doi          = "10.4204/EPTCS.25.11",
)
@book(Mueller2000,
 author       = "Silvia M. M{\"u}ller and Wolfgang J. Paul",
 year         = "2000",
 title        = "Computer architecture: complexity and correctness",
 publisher    = "Springer",
)
@inproceedings(DBLP:conf/sat/NadelR10,
 author       = "Alexander Nadel and Vadim Ryvchin",
 year         = "2010",
 title        = "Assignment Stack Shrinking",
 editor       = "Strichman and Szeider",
 pages        = "375--381",
 doi          = "10.1007/978-3-642-14186-7_35",
)
@misc(SATRace2010,
 author       = "Carsten Sinz (organiser)",
 title        = "SAT-Race 2010",
 howpublished = "\burl {http://baldur.iti.uka.de/sat-race-2010/}",
)
@article(DBLP:journals/iandc/Parberry94,
 author       = "Ian Parberry",
 year         = "1994",
 title        = "A Guide for New Referees in Theoretical Computer Science",
 journal      = "Inf. Comput.",
 volume       = "112",
 number       = "1",
 pages        = "96--116",
)
@inproceedings(DBLP:conf/vmcai/PitermanPS06,
 author       = "Nir Piterman and Amir Pnueli and Yaniv Sa'ar",
 year         = "2006",
 title        = "Synthesis of Reactive(1) Designs",
 editor       = "E. Allen Emerson and Kedar S. Namjoshi",
 booktitle    = "VMCAI",
 series       = "LNCS",
 volume       = "3855",
 publisher    = "Springer",
 pages        = "364--380",
 doi          = "10.1007/11609773_24",
)
@inproceedings(DBLP:conf/focs/Pnueli77,
 author       = "Amir Pnueli",
 year         = "1977",
 title        = "The Temporal Logic of Programs",
 booktitle    = "FOCS",
 publisher    = "IEEE",
 pages        = "46--57",
)
@inproceedings(DBLP:conf/popl/PnueliR89,
 author       = "Amir Pnueli and Roni Rosner",
 year         = "1989",
 title        = "On the Synthesis of a Reactive Module",
 booktitle    = "POPL",
 pages        = "179--190",
)
@inproceedings(DBLP:conf/icalp/PnueliR89,
 author       = "Amir Pnueli and Roni Rosner",
 year         = "1989",
 title        = "On the Synthesis of an Asynchronous Reactive Module",
 editor       = "\write \rebib { editor = "Ausiello",}",
 pages        = "652--671",
)
@inproceedings(DBLP:conf/cav/PnueliSZ10,
 author       = "Amir Pnueli and Yaniv Sa'ar and Lenore D. Zuck",
 year         = "2010",
 title        = "Jtlv: A Framework for Developing Verification Algorithms",
 editor       = "\write \rebib { editor = "Touili",}",
 pages        = "171--174",
 doi          = "10.1007/978-3-642-14295-6_18",
)
@proceedings(DBLP:conf/spin/2010,
 editor       = "Jaco van de Pol and Michael Weber",
 year         = "2010",
 title        = "Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010",
 series       = "LNCS",
 volume       = "6349",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-16164-3",
)
@article(DBLP:journals/sttt/RozierV10,
 author       = "Kristin Y. Rozier and Moshe Y. Vardi",
 year         = "2010",
 title        = "{LTL} satisfiability checking",
 journal      = "STTT",
 volume       = "12",
 number       = "2",
 pages        = "123--137",
 doi          = "10.1007/s10009-010-0140-3",
)
@phdthesis(phd-safra,
 author       = "Shmuel Safra",
 year         = "1989",
 title        = "Complexity of Automata on Infinite Objects",
 school       = "Weizmann Institute of Science, Rehovot, Israel",
)
@inproceedings(DBLP:conf/atva/ScheweF07a,
 author       = "Sven Schewe and Bernd Finkbeiner",
 year         = "2007",
 title        = "Bounded Synthesis",
 editor       = "Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura",
 booktitle    = "ATVA",
 series       = "LNCS",
 volume       = "4762",
 publisher    = "Springer",
 pages        = "474--488",
 doi          = "10.1007/978-3-540-75596-8_33",
)
@inproceedings(DBLP:conf/fmcad/SohailS09,
 author       = "Saqib Sohail and Fabio Somenzi",
 year         = "2009",
 title        = "Safety first: A two-stage algorithm for LTL games",
 booktitle    = "FMCAD",
 publisher    = "IEEE",
 pages        = "77--84",
 doi          = "10.1109/FMCAD.2009.5351138",
)
@inproceedings(DBLP:conf/vmcai/SohailSR08,
 author       = "Saqib Sohail and Fabio Somenzi and Kavita Ravi",
 year         = "2008",
 title        = "A Hybrid Algorithm for LTL Games",
 editor       = "Francesco Logozzo and Doron Peled and Lenore D. Zuck",
 booktitle    = "VMCAI",
 series       = "LNCS",
 volume       = "4905",
 publisher    = "Springer",
 pages        = "309--323",
 doi          = "10.1007/978-3-540-78163-9_26",
)
@misc(Somenzi98cudd:cu,
 author       = "Fabio Somenzi",
 year         = "2009",
 title        = "{CUDD}: {CU Decision Diagram} Package Release 2.4.2",
)
@inproceedings(DBLP:conf/cav/SomenziB00,
 author       = "Fabio Somenzi and Roderick Bloem",
 year         = "2000",
 title        = "Efficient B{\"u}chi Automata from LTL Formulae",
 editor       = "Emerson and Sistla",
 pages        = "248--263",
)
@proceedings(DBLP:conf/sat/2010,
 editor       = "Ofer Strichman and Stefan Szeider",
 year         = "2010",
 title        = "Theory and Applications of Satisfiability Testing (SAT)",
 series       = "LNCS",
 volume       = "6175",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-14186-7",
)
@article(DBLP:journals/computer/Tichy98,
 author       = "Walter F. Tichy",
 year         = "1998",
 title        = "Should Computer Scientists Experiment More?",
 journal      = "IEEE Computer",
 volume       = "31",
 number       = "5",
 pages        = "32--40",
)
@proceedings(DBLP:conf/cav/2010,
 editor       = "Tayssir Touili and Byron Cook and Paul Jackson",
 year         = "2010",
 title        = "The 22nd International Conference on Computer Aided Verification (CAV)",
 series       = "LNCS",
 volume       = "6174",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-14295-6",
)
@inproceedings(Vardi1995,
 author       = "Moshe Y. Vardi",
 year         = "1995",
 title        = "An Automata-Theoretic Approach to Linear Temporal Logic",
 editor       = "Faron Moller and Graham M. Birtwistle",
 booktitle    = "Banff Higher Order Workshop",
 series       = "LNCS",
 volume       = "1043",
 publisher    = "Springer",
)
@inproceedings(DBLP:conf/stoc/VardiS85,
 author       = "Moshe Y. Vardi and Larry J. Stockmeyer",
 year         = "1985",
 title        = "Improved Upper and Lower Bounds for Modal Logics of Programs: Preliminary Report",
 booktitle    = "STOC",
 publisher    = "ACM",
 pages        = "240--251",
)