@article(ap07,
 author       = "Luca de Alfaro and Pritam Roy",
 year         = "2010",
 title        = "Solving games via three-valued abstraction refinement",
 journal      = "Information and Computation",
 volume       = "208",
 number       = "6",
 pages        = "666--676",
 doi          = "10.1016/j.ic.2009.05.007",
)
@inproceedings(bks14,
 author       = "Roderick Bloem and Robert K{\"o}nighofer and Martina Seidl",
 year         = "2014",
 title        = "SAT-Based Synthesis Methods for Safety Specs",
 booktitle    = "VMCAI",
 series       = "LNCS",
 volume       = "8318",
 publisher    = "Springer",
 pages        = "1--20",
 doi          = "10.1007/978-3-642-54013-4\_1",
)
@article(bryant86,
 author       = "Randal E. Bryant",
 year         = "1986",
 title        = "Graph-based algorithms for boolean function manipulation",
 journal      = "Computers, IEEE Transactions on",
 volume       = "100",
 number       = "8",
 pages        = "677--691",
 doi          = "10.1109/TC.1986.1676819",
)
@inproceedings(bcl91,
 author       = "Jerry R. Burch and Edmund M. Clarke and David E. Long",
 year         = "1991",
 title        = "Symbolic Model Checking with Partitioned Transistion Relations",
 booktitle    = "VLSI",
 pages        = "49--58",
)
@inproceedings(cgjlv00,
 author       = "Edmund Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith",
 year         = "2000",
 title        = "Counterexample-guided abstraction refinement",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "1855",
 publisher    = "Springer",
 pages        = "154--169",
 doi          = "10.1007/10722167\_15",
)
@inproceedings(cgt04,
 author       = "Edmund Clarke and Orna Grumberg and Muralidhar Talupur and Dong Wang",
 year         = "2003",
 title        = "High level verification of control intensive systems using predicate abstraction",
 booktitle    = "MEMOCODE",
 publisher    = "IEEE",
 pages        = "55--64",
 doi          = "10.1109/MEMCOD.2003.1210089",
)
@inproceedings(cbm90,
 author       = "Olivier Coudert and Christian Berthet and Jean Christophe Madre",
 year         = "1990",
 title        = "Verification of synchronous sequential machines based on symbolic execution",
 booktitle    = "Automatic verification methods for finite state systems",
 series       = "LNCS",
 volume       = "407",
 publisher    = "Springer",
 pages        = "365--373",
 doi          = "10.1007/3-540-52148-8\_30",
)
@inproceedings(cm90,
 author       = "Olivier Coudert and Jean Christophe Madre",
 year         = "1990",
 title        = "A Unified Framework for the Formal Verification of Sequential Circuits",
 booktitle    = "ICCAD",
 pages        = "126--129",
)
@inproceedings(cmb91,
 author       = "Olivier Coudert and Jean Christophe Madre and Christian Berthet",
 year         = "1991",
 title        = "Verifying temporal properties of sequential machines without building their state diagrams",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "531",
 publisher    = "Springer",
 pages        = "23--32",
 doi          = "10.1007/BFb0023716",
)
@inproceedings(cc77,
 author       = "Patrick Cousot and Radhia Cousot",
 year         = "1977",
 title        = "Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints",
 booktitle    = "POPL",
 publisher    = "ACM",
 pages        = "238--252",
 doi          = "10.1145/512950.512973",
)
@inproceedings(ehlers10,
 author       = "R{\"u}diger Ehlers",
 year         = "2010",
 title        = "Symbolic Bounded Synthesis",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "6174",
 publisher    = "Springer",
 pages        = "365--379",
 doi          = "10.1007/s10703-011-0137-x",
)
@inproceedings(ej91,
 author       = "E. Allen Emerson and Charanjit S. Jutla",
 year         = "1991",
 title        = "Tree automata, mu-calculus and determinacy",
 booktitle    = "FOCS",
 organization = "IEEE",
 pages        = "368--377",
 doi          = "10.1109/SFCS.1991.185392",
)
@inproceedings(fjr09,
 author       = "Emmanuel Filiot and Naiyong Jin and Jean-Fran{\c {c}}ois Raskin",
 year         = "2009",
 title        = "An Antichain Algorithm for {LTL} Realizability",
 booktitle    = "{CAV}",
 series       = "{LNCS}",
 volume       = "5643",
 publisher    = "Springer",
 pages        = "263--277",
 doi          = "10.1007/978-3-642-02658-4\_22",
)
@inproceedings(gradel04,
 author       = "Erich Gr{\"a}del",
 year         = "2004",
 title        = "Positional Determinacy of Infinite Games",
 booktitle    = "STACS",
 series       = "LNCS",
 volume       = "2996",
 publisher    = "Springer",
 pages        = "4--18",
 doi          = "10.1007/978-3-540-24749-4\_2",
)
@inproceedings(gs97,
 author       = "Susanne Graf and Hassen Sa{\"\i }di",
 year         = "1997",
 title        = "Construction of abstract state graphs with PVS",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "1254",
 publisher    = "Springer",
 pages        = "72--83",
 doi          = "10.1007/3-540-63166-6\_10",
)
@inproceedings(hjm03,
 author       = "Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
 year         = "2003",
 title        = "Counterexample-guided control",
 booktitle    = "ICALP",
 series       = "LNCS",
 volume       = "2719",
 publisher    = "Springer",
 pages        = "886--902",
 doi          = "10.1007/3-540-45061-0\_69",
)
@inproceedings(hmmr00,
 author       = "Thomas A. Henzinger and Rupak Majumdar and Freddy Y. C. Mang and Jean-Fran\c {c}ois Raskin",
 year         = "2000",
 title        = "Abstract Interpretation of Game Properties",
 booktitle    = "SAS",
 pages        = "220--239",
 doi          = "10.1007/978-3-540-45099-3\_12",
)
@inproceedings(hbbm97,
 author       = "Youpyo Hong and Peter A Beerel and Jerry R Burch and Kenneth L McMillan",
 year         = "1997",
 title        = "Safe BDD minimization using don't cares",
 booktitle    = "Proceedings of the 34th annual Design Automation Conference",
 organization = "ACM",
 pages        = "208--213",
 doi          = "10.1145/266021.266068",
)
@inproceedings(kurshan94,
 author       = "Robert P. Kurshan",
 year         = "1994",
 title        = "Automata-theoretic verification of coordinating processes",
 booktitle    = "11th International Conference on Analysis and Optimization of Systems Discrete Event Systems",
 organization = "Springer",
 pages        = "16--28",
 doi          = "10.1007/BFb0033528",
)
@article(mccluskey56,
 author       = "Edward J. McCluskey",
 year         = "1956",
 title        = "Minimization of Boolean Functions*",
 journal      = "Bell system technical Journal",
 volume       = "35",
 number       = "6",
 pages        = "1417--1444",
 doi          = "10.1002/j.1538-7305.1956.tb03835.x",
)
@inproceedings(nlbrw14,
 author       = "Nina Narodytska and Alexander Legg and Fahiem Bacchus and Leonid Ryzhyk and Adam Walker",
 year         = "2014",
 title        = "Solving Games without Controllable Predecessor",
 booktitle    = "CAV",
 organization = "Springer",
)
@article(py86,
 author       = "Christos H. Papadimitriou and Mihalis Yannakakis",
 year         = "1986",
 title        = "A note on succinct representations of graphs",
 journal      = "Information and Control",
 volume       = "71",
 number       = "3",
 pages        = "181 -- 185",
 doi          = "10.1016/S0019-9958(86)80009-2",
)
@article(sw96,
 author       = "Martin Sauerhoff and Ingo Wegener",
 year         = "1996",
 title        = "On the complexity of minimizing the OBDD size for incompletely specified functions",
 journal      = "IEEE Trans. on CAD of Integrated Circuits and Systems",
 volume       = "15",
 number       = "11",
 pages        = "1435--1437",
 doi          = "10.1109/43.543775",
)
@article(ss09,
 author       = "Saqib Sohail and Fabio Somenzi",
 year         = "2009",
 title        = "Safety first: A two-stage algorithm for LTL games",
 journal      = "FMCAD",
 pages        = "77--84",
 doi          = "10.1007/s10009-012-0224-3",
)
@incollection(somenzi99,
 author       = "Fabio Somenzi",
 year         = "1999",
 title        = "Binary Decision Diagrams",
 booktitle    = "Calculational system design",
 volume       = "173",
 publisher    = "IOS Press",
 pages        = "303",
)
@article(tarski55,
 author       = "Alfred Tarski",
 year         = "1955",
 title        = "A lattice-theoretical fixpoint theorem and its applications",
 journal      = "Pacific journal of Mathematics",
 volume       = "5",
 number       = "2",
 pages        = "285--309",
 doi          = "10.2140/pjm.1955.5.285",
)
@inproceedings(thomas95,
 author       = "Wolfgang Thomas",
 year         = "1995",
 title        = "On the synthesis of strategies in infinite games",
 booktitle    = "STACS",
 organization = "Springer",
 pages        = "1--13",
 doi          = "10.1007/3-540-59042-0\_57",
)