@misc(AIGER,
 author       = {Armin Biere},
 title        = {AIGER format and toolbox},
 url          = {http://fmv.jku.at/aiger/},
)
@misc(AIGEROLD,
 author       = {Armin Biere},
 title        = {AIGER format version 20070427},
 url          = {http://fmv.jku.at/aiger/FORMAT-20070427.pdf},
)
@misc(smvflatten,
 author       = {Armin Biere},
 title        = {{\sf smvflatten}},
 url          = {http://fmv.jku.at/smvflatten/},
)
@article(AIGERNEW,
 author       = {Armin Biere and Keijo Heljanko and Siert Wieringa},
 year         = {2011},
 title        = {AIGER 1.9 and Beyond},
 url          = {http://www.fmv.jku.at/hwmcc11/beyond1.pdf},
)
@misc(IIMC,
 author       = {Aaron Bradley and Arlen Cox and Michael Dooley and Zyad Hassan and Fabio Somenzi and Yan Zhang},
 title        = {IIMC},
 url          = {http://ecee.colorado.edu/wpmu/iimc/},
)
@incollection(VIS,
 author       = {RobertK. Brayton and GaryD. Hachtel and Sangiovanni-Vincentelli, Alberto and Fabio Somenzi and Adnan Aziz and Szu-Tsung Cheng and Stephen Edwards and Sunil Khatri and Yuji Kukimoto and Abelardo Pardo and Shaz Qadeer and RajeevK. Ranjan and Shaker Sarwary and ThomasR. Staple and Gitanjali Swamy and Tiziano Villa},
 year         = {1996},
 title        = {VIS: A system for verification and synthesis},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {1102},
 pages        = {428--432},
 doi          = {10.1007/3-540-61474-5\_95},
)
@incollection(SMV,
 author       = {Alessandro Cimatti and Edmund Clarke and Enrico Giunchiglia and Fausto Giunchiglia and Marco Pistore and Marco Roveri and Roberto Sebastiani and Armando Tacchella},
 year         = {2002},
 title        = {NuSMV 2: An OpenSource Tool for Symbolic Model Checking},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {2404},
 pages        = {359--364},
 doi          = {10.1007/3-540-45657-0\_29},
)
@article(HuffmanCoding,
 author       = {D.A. Huffman},
 year         = {1952},
 title        = {A Method for the Construction of Minimum-Redundancy Codes},
 journal      = {Proceedings of the IRE},
 volume       = {40},
 number       = {9},
 pages        = {1098--1101},
 doi          = {10.1109/JRPROC.1952.273898},
)
@misc(SYNTCOMP,
 author       = {Swen Jacobs},
 year         = {2014},
 title        = {Extended AIGER Format for Synthesis (v0.1)},
 note         = {ArXiv:1405.5793},
)
@misc(ltl2aig,
 author       = {Guillermo A. Perez},
 title        = {{\sf ltl2aig}},
 url          = {https://github.com/gaperez64/acacia_ltl2aig},
)
@inproceedings(GR1,
 author       = {Nir Piterman and Amir Pnueli and Yaniv Sa’ar},
 year         = {2006},
 title        = {Synthesis of reactive (1) designs},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation},
 organization = {Springer},
 pages        = {364--380},
 doi          = {10.1007/11609773\_24},
)
@misc(Patterns-to-GR1,
 author       = {Jan Oliver Ringert},
 year         = {2015},
 title        = {Extensible Support for Specification Patterns in GR(1) Synthesis (Work in Progress)},
 howpublished = {Young Researchers' Conference ``Frontiers of Formal Methods''},
 url          = {http://ffm2015.rwth-aachen.de/proceedings.php},
)
@incollection(GOAL,
 author       = {Yih-Kuen Tsay and Yu-Fang Chen and Ming-Hsien Tsai and Kang-Nien Wu and Wen-Chin Chan},
 year         = {2007},
 title        = {GOAL: A graphical tool for manipulating B{\"u}chi automata and temporal formulae},
 booktitle    = {TACAS},
 publisher    = {Springer},
 pages        = {466--471},
 doi          = {10.1007/978-3-540-71209-1\_35},
)
@misc(LDL,
 author       = {M. Y. Vardi},
 year         = {2011},
 title        = {The rise and fall of linear time logic},
 howpublished = {2nd Int’l Symp. on Games, Automata, Logics and Formal Verification},
 note         = {Invited talk},
)