@inproceedings(Alfaro_GJ_04,
 author       = {Luca de Alfaro and Patrice Godefroid and Radha Jagadeesan},
 year         = {2004},
 title        = {Three-valued abstractions of games: uncertainty, but with precision},
 booktitle    = {LICS},
 address      = {Turku, Finland},
 pages        = {170--179},
 doi          = {10.1109/lics.2004.1319611},
)
@inproceedings(Alfaro_Roy_07,
 author       = {Luca de Alfaro and Pritam Roy},
 year         = {2007},
 title        = {Solving Games Via Three-Valued Abstraction Refinement},
 booktitle    = {CONCUR},
 address      = {Lisboa, Portugal},
 pages        = {74--89},
 doi          = {10.1007/978-3-540-74407-8\_6},
)
@article(Alur_BHQR_01,
 author       = {R. Alur and R. K. Brayton and T. A. Henzinger and S. Qadeer and S. K. Rajamani},
 year         = {2001},
 title        = {Partial-Order Reduction in Symbolic State-Space Exploration},
 journal      = {Formal Methods in System Design},
 volume       = {18},
 number       = {2},
 pages        = {97--116},
 doi          = {10.1023/A:1008767206905},
)
@article(Amani_CDLORZ_14,
 author       = {Sidney Amani and Peter Chubb and Alastair Donaldson and Alexander Legg and Keng Chai Ong and Leonid Ryzhyk and Yanjin Zhu},
 year         = {2014},
 title        = {Automatic Verification of Active Device Drivers},
 journal      = {{ACM} Operating Systems Review},
 volume       = {48},
 number       = {1},
 doi          = {10.1145/2626401.2626424},
)
@inproceedings(Ball_BCLLMORU_06,
 author       = {Thomas Ball and Ella Bounimova and Byron Cook and Vladimir Levin and Jakob Lichtenberg and Con McGarvey and Bohus Ondrusek and Sriram K. Rajamani and Abdullah Ustuner},
 year         = {2006},
 title        = {Thorough Static Analysis of Device Drivers},
 booktitle    = {1st EuroSys Conference},
 address      = {Leuven, Belgium},
 pages        = {73--85},
 doi          = {10.1145/1217935.1217943},
)
@inproceedings(Bloem_CGHKRSS_10,
 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},
 address      = {Edinburgh, UK},
 pages        = {425--429},
 doi          = {10.1007/978-3-642-14295-6\_37},
)
@inproceedings(Bloem_EKKL_14,
 author       = {Roderick Bloem and Uwe Egly and Patrick Klampfl and Robert Koenighofer and Florian Lonsing},
 year         = {2014},
 title        = {SAT-Based Methods for Circuit Synthesis},
 booktitle    = {FMCAD},
 address      = {Lausanne, Switzerland},
 doi          = {10.1109/FMCAD.2014.6987592},
)
@article(Bloem_KS_13,
 author       = {Roderick Bloem and Robert K{\"o}nighofer and Martina Seidl},
 year         = {2013},
 title        = {{SAT}-Based Synthesis Methods for Safety Specs},
 journal      = {CoRR},
 volume       = {abs/1311.3530},
)
@inproceedings(Bloem2014,
 author       = {Roderick Bloem and Robert K{\"o}nighofer and Martina Seidl},
 year         = {2014},
 title        = {{SAT}-Based Synthesis Methods for Safety Specs},
 booktitle    = {VMCAI'14},
 publisher    = {Springer Berlin Heidelberg},
 address      = {San Diego, CA, USA},
 pages        = {1--20},
 doi          = {10.1007/978-3-642-54013-4\_1},
)
@inproceedings(Bohy_BFJR_12,
 author       = {Aaron Bohy and V{\'{e}}ronique Bruy{\`{e}}re and Emmanuel Filiot and Naiyong Jin and Jean{-}Fran{\c{c}}ois Raskin},
 year         = {2012},
 title        = {Acacia+, a Tool for {LTL} Synthesis},
 booktitle    = {CAV},
 address      = {Berkeley, California, USA},
 pages        = {652--657},
 doi          = {10.1007/978-3-642-31424-7\_45},
)
@article(Bryant_86,
 author       = {Randal E. Bryant},
 year         = {1986},
 title        = {Graph-Based Algorithms for Boolean Function Manipulation},
 journal      = {IEEE Transactions on Computers},
 volume       = {35},
 pages        = {677--691},
 doi          = {10.1109/TC.1986.1676819},
)
@inproceedings(Cai_Gajski_03,
 author       = {Lukai Cai and Daniel Gajski},
 year         = {2003},
 title        = {Transaction level modeling: an overview},
 booktitle    = {"1st International Conference on Hardware/Software Codesign and System Synthesis"},
 address      = {Newport Beach, CA, USA},
 pages        = {19--24},
 doi          = {10.1145/944650.944651},
)
@inproceedings(Case_BM_06,
 author       = {Michael L. Case and Alan Mishchenko and Robert K. Brayton},
 year         = {2006},
 title        = {Inductively Finding a Reachable State Space Over-Approximation},
 booktitle    = {Proceedings of the 15th International Workshop on Logic and Synthesis},
)
@inproceedings(Cassez_DFLL_05,
 author       = {Franck Cassez and Alexandre David and Emmanuel Fleury and Kim G. Larsen and Didier Lime},
 year         = {2005},
 title        = {Efficient On-the-fly Algorithms for the Analysis of Timed Games},
 booktitle    = {CONCUR},
 address      = {San Francisco, CA, USA},
 pages        = {66--80},
 doi          = {10.1007/11539452\_9},
)
@inproceedings(Cerny_HRRT_13,
 author       = {Pavol Cerny and Thomas Henzinger and Arjun Radhakrishna and Leonid Ryzhyk and Thorsten Tarrach},
 year         = {2013},
 title        = {Efficient synthesis for concurrency by semantics-preserving transformations},
 booktitle    = {CAV},
 address      = {Saint Petersburg, Russia},
 doi          = {10.1007/978-3-642-39799-8\_68},
)
@inproceedings(Cerny_HRRT_14,
 author       = {Pavol Cerny and Thomas Henzinger and Arjun Radhakrishna and Leonid Ryzhyk and Thorsten Tarrach},
 year         = {2014},
 title        = {Regression-free synthesis for concurrency},
 booktitle    = {CAV},
 address      = {Vienna, Austria},
 doi          = {10.1007/978-3-319-08867-9\_38},
)
@inproceedings(Chatterjee_RR_12,
 author       = {Krishnendu Chatterjee and Mickael Randour and Jean-Fran\c{c}ois Raskin},
 year         = {2012},
 title        = {Strategy Synthesis for Multi-dimensional Quantitative Objectives},
 booktitle    = {CONCUR},
 address      = {Newcastle, UK},
 pages        = {115--131},
 doi          = {10.1007/978-3-642-32940-1\_10},
)
@inproceedings(Chen_MK_07,
 author       = {Mingsong Chen and Prabhat Mishra and Dhrubajyoti Kalita},
 year         = {2007},
 title        = {Towards {RTL} test generation from {SystemC} {TLM} specifications},
 booktitle    = {HLDVT'07},
 pages        = {91--96},
 doi          = {10.1109/hldvt.2007.4392793},
)
@inproceedings(Cheng_KLB_11,
 author       = {Chih{-}Hong Cheng and Alois Knoll and Michael Luttenberger and Christian Buckl},
 year         = {2011},
 title        = {{GAVS+:} An Open Platform for the Research of Algorithmic Game Solving},
 booktitle    = {TACAS},
 address      = {Saarbr\"ucken, Germany},
 pages        = {258--261},
 doi          = {10.1007/978-3-642-19835-9\_22},
)
@article(Chipounov_KC_12,
 author       = {Vitaly Chipounov and Volodymyr Kuznetsov and George Candea},
 year         = {2012},
 title        = {The {S2E} Platform: Design, Implementation, and Applications},
 journal      = {ACM Transactions on Computer Systems},
 volume       = {30},
 number       = {1},
 pages        = {2:1--2:49},
 doi          = {10.1145/2110356.2110358},
)
@inproceedings(Chou_YCHE_01,
 author       = {Andy Chou and Jun-Feng Yang and Benjamin Chelf and Seth Hallem and Dawson Engler},
 year         = {2001},
 title        = {An Empirical Study of Operating Systems Errors},
 booktitle    = {18th {ACM} Symposium on Operating Systems Principles},
 address      = {Lake Louise, Alta, Canada},
 pages        = {73--88},
 doi          = {10.1145/502059.502042},
)
@article(Clarke_GJLV_03,
 author       = {Edmund Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},
 year         = {2003},
 title        = {Counterexample-guided abstraction refinement for symbolic model checking},
 journal      = {Journal of the ACM},
 volume       = {50},
 pages        = {752--794},
 doi          = {10.1145/876638.876643},
)
@article(Clarke_KSY_04,
 author       = {Edmund M. Clarke and Daniel Kroening and Natasha Sharygina and Karen Yorav},
 year         = {2004},
 title        = {Predicate Abstraction of {ANSI-C} Programs Using {SAT}},
 journal      = {Formal Methods in System Design},
 volume       = {25},
 number       = {2-3},
 pages        = {105--127},
 doi          = {10.1023/B:FORM.0000040025.89719.f3},
)
@inproceedings(Desai_GJQRZ_13,
 author       = {Ankush Desai and Vivek Gupta and Ethan Jackson and Shaz Qadeer and Sriram Rajamani and Damien Zufferey},
 year         = {2013},
 title        = {{P}: safe asynchronous event-driven programming},
 booktitle    = {34th annual ACM SIGPLAN conference on Programming Language Design and Implementation},
 address      = {Seattle, Washington, USA},
 pages        = {321--332},
 doi          = {10.1145/2491956.2462184},
)
@inproceedings(Dimitrova_Finkbeiner_08,
 author       = {Rayna Dimitrova and Bernd Finkbeiner},
 year         = {2008},
 title        = {Abstraction Refinement for Games with Incomplete Information},
 booktitle    = {FSTTCS},
 address      = {Bangalore, India},
)
@inproceedings(Dimitrova_Finkbeiner_12,
 author       = {Rayna Dimitrova and Bernd Finkbeiner},
 year         = {2012},
 title        = {Counterexample-Guided Synthesis of Observation Predicates},
 booktitle    = {FORMATS},
 address      = {London, UK},
 pages        = {107--122},
 doi          = {10.1007/978-3-642-33365-1\_9},
)
@inproceedings(Ehlers_10,
 author       = {R\"{u}diger Ehlers},
 year         = {2010},
 title        = {Symbolic Bounded Synthesis},
 booktitle    = {CAV},
 address      = {Edinburgh, UK},
 doi          = {10.1007/978-3-642-14295-6\_33},
)
@inproceedings(Ehlers_KH_12,
 author       = {R{\"{u}}diger Ehlers and Robert K{\"{o}}nighofer and Georg Hofferek},
 year         = {2012},
 title        = {Symbolically synthesizing small circuits},
 booktitle    = {FMCAD},
 address      = {Cambridge, UK},
 pages        = {91--100},
)
@inproceedings(Flanagan_Qadeer_02,
 author       = {Cormac Flanagan and Shaz Qadeer},
 year         = {2002},
 title        = {Predicate Abstraction for Software Verification},
 booktitle    = {29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 address      = {Portland, Oregon},
 pages        = {191--202},
 doi          = {10.1145/503272.503291},
)
@inproceedings(Ganapathi_GP_06,
 author       = {Archana Ganapathi and Viji Ganapathi and David Patterson},
 year         = {2006},
 title        = {{Windows XP} Kernel Crash Analysis},
 booktitle    = {20th USENIX Large Installation System Administration Conference},
 address      = {Washington, DC, USA},
 pages        = {101--111},
)
@book(Grumberg_Veith_08,
 editor       = {Orna Grumberg and Helmut Veith},
 year         = {2008},
 title        = {25 Years of Model Checking: History, Achievements, Perspectives},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-540-69850-0},
)
@inproceedings(Henzinger_JM_03,
 author       = {Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar},
 year         = {2003},
 title        = {Counterexample-guided control},
 booktitle    = {ICALP},
 address      = {Eindhoven, The Netherlands},
 pages        = {886--902},
 doi          = {10.1007/3-540-45061-0\_69},
)
@misc(cofluent,
 author       = {{Intel Corporation}},
 title        = {CoFluent Technolofy},
 howpublished = {\url{http://www.intel.com/content/www/us/en/cofluent/cofluent-difference.html}},
)
@article(Jacobs_14,
 author       = {Swen Jacobs},
 year         = {2014},
 title        = {Extended {AIGER} Format for Synthesis},
 journal      = {CoRR},
 volume       = {abs/1405.5793},
)
@inproceedings(Jobstmann_Bloem_06,
 author       = {Barbara Jobstmann and Roderick Bloem},
 year         = {2006},
 title        = {Optimizations for {LTL} Synthesis},
 booktitle    = {FMCAD},
 address      = {San Jose, CA, USA},
 pages        = {117--124},
 doi          = {10.1109/fmcad.2006.22},
)
@inproceedings(Jobstmann_GWB_07,
 author       = {Barbara Jobstmann and Stefan J. Galler and Martin Weiglhofer and Roderick Bloem},
 year         = {2007},
 title        = {Anzu: {A} Tool for Property Synthesis},
 booktitle    = {CAV},
 address      = {Berlin, Germany},
 pages        = {258--262},
 doi          = {10.1007/978-3-540-73368-3\_29},
)
@inproceedings(Kadav_RS_09,
 author       = {Asim Kadav and Matthew J. Renzelmann and Michael M. Swift},
 year         = {2009},
 title        = {Tolerating Hardware Device Failures in Software},
 booktitle    = {22nd ACM Symposium on Operating Systems Principles},
 address      = {Big Sky, MT, USA},
 doi          = {10.1145/1629575.1629582},
)
@inproceedings(Klein_EHACDEEKNSTW_09,
 author       = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and June Andronick and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood},
 year         = {2009},
 title        = {{seL4}: Formal Verification of an {OS} Kernel},
 booktitle    = {22nd {ACM} Symposium on Operating Systems Principles},
 address      = {Big Sky, MT, USA},
 pages        = {207--220},
 doi          = {10.1145/1629575.1629596},
)
@article(Kneuss_KKS_13,
 author       = {Etienne Kneuss and Viktor Kuncak and Ivan Kuraj and Philippe Suter},
 year         = {2013},
 title        = {On Integrating Deductive Synthesis and Verification Systems},
 journal      = {CoRR},
 volume       = {abs/1304.5661},
)
@inproceedings(Koninghofer_HB_09,
 author       = {Robert K{\"{o}}nighofer and Georg Hofferek and Roderick Bloem},
 year         = {2009},
 title        = {Debugging formal specifications using simple counterstrategies},
 booktitle    = {FMCAD},
 address      = {Austin, Texas, USA},
 pages        = {152--159},
 doi          = {10.1109/fmcad.2009.5351127},
)
@article(Konighofer_HB_13,
 author       = {Robert K{\"{o}}nighofer and Georg Hofferek and Roderick Bloem},
 year         = {2013},
 title        = {Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies},
 journal      = {STTT},
 volume       = {15},
 number       = {5-6},
 pages        = {563--583},
 doi          = {10.1007/s10009-011-0221-y},
)
@incollection(Kupferman_Vardi_2000,
 author       = {Orna Kupferman and Moshe Vardi},
 year         = {2000},
 title        = {Synthesis with Incomplete Information},
 booktitle    = {Advances in Temporal Logic},
 volume       = {16},
 publisher    = {Springer Netherlands},
 pages        = {109--127},
 doi          = {10.1007/978-94-015-9586-5\_6},
)
@article(Leslie_CFGGMPSEH_05,
 author       = {Ben Leslie and Peter Chubb and FitzRoy-Dale, Nicholas and Stefan G\"{o}tz and Charles Gray and Luke Macpherson and Daniel Potts and Yueting (Rita) Shen and Kevin Elphinstone and Gernot Heiser},
 year         = {2005},
 title        = {User-level Device Drivers: Achieved Performance},
 journal      = {Journal of Computer Science and Technology},
 volume       = {20},
 number       = {5},
 pages        = {654--664},
 doi          = {10.1007/s11390-005-0654-4},
)
@inproceedings(LeVasseur_USG_04,
 author       = {Joshua LeVasseur and Volkmar Uhlig and Jan Stoess and Stefan G\"{o}tz},
 year         = {2004},
 title        = {Unmodified Device Driver Reuse and Improved System Dependability via Virtual Machines},
 booktitle    = {6th Symposium on Operating Systems Design and Implementation},
 address      = {San Francisco, CA, USA},
 pages        = {17--30},
)
@inproceedings(Merillon_RCMM_00,
 author       = {Fabrice M\'{e}rillon and Laurent R\'{e}veill\`{e}re and Charles Consel and Renaud Marlet and Gilles Muller},
 year         = {2000},
 title        = {Devil: An {IDL} for hardware programming},
 booktitle    = {4th USENIX Symposium on Operating Systems Design and Implementation},
 address      = {San Diego, CA, USA},
 pages        = {17--30},
)
@inproceedings(Morgenstern_GS_13,
 author       = {Andreas Morgenstern and Manuel Gesell and Klaus Schneider},
 year         = {2013},
 title        = {Solving Games Using Incremental Induction},
 booktitle    = {IFM},
 address      = {Turku, Finland},
 pages        = {177--191},
 doi          = {10.1007/978-3-642-38613-8\_13},
)
@inproceedings(Moskewicz_MZZM_01,
 author       = {Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao Zhang and Sharad Malik},
 year         = {2001},
 title        = {Chaff: engineering an efficient {SAT} solver},
 booktitle    = {DAC},
 address      = {Las Vegas, NV, USA},
 pages        = {530--535},
 doi          = {10.1109/dac.2001.935565},
)
@inproceedings(Narodytska_LBRW_14,
 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},
 address      = {Vienna, Austria},
 doi          = {10.1007/978-3-319-08867-9\_35},
)
@inproceedings(Naujokat_LS_12,
 author       = {Stefan Naujokat and Anna-Lena Lamprecht and Bernhard Steffen},
 year         = {2012},
 title        = {Loose Programming with {PROPHETS}},
 booktitle    = {FASE'12},
 address      = {Tallinn, Estonia},
 pages        = {94--98},
 doi          = {10.1007/978-3-642-28872-2\_7},
)
@inproceedings(ONils_OJ_98,
 author       = {Mattias O'Nils and Johnny \"{O}berg and Axel Jantsch},
 year         = {1998},
 title        = {Grammar Based Modelling and Synthesis of Device Drivers and Bus Interfaces},
 address      = {Washington, DC, USA},
 doi          = {10.1109/EURMIC.1998.711776},
)
@misc(uart,
 title        = {{16550 UART core}},
 howpublished = {\url{http://opencores.org/project,a_vhd_16550_uart}},
)
@inproceedings(Palix_GSCLM_11,
 author       = {Nicolas Palix and Ga\"{e}l Thomas and Suman Saha and Christophe Calv\`{e}s and Julia Lawall and Gilles Muller},
 year         = {2011},
 title        = {Faults in {Linux}: ten years later},
 booktitle    = {16th International Conference on Architectural Support for Programming Languages and Operating Systems},
 address      = {Newport Beach, CA, USA},
 pages        = {305--318},
 doi          = {10.1145/1950365.1950401},
)
@inproceedings(Piterman_PS_06,
 author       = {Nir Piterman and Amir Pnueli and Yaniv Sa'ar},
 year         = {2006},
 title        = {Synthesis of {Reactive}(1) designs},
 booktitle    = {7th International Conference on Verification, Model Checking and Abstract Interpretation},
 pages        = {364--380},
 doi          = {10.1007/11609773\_24},
)
@inproceedings(Pnueli_Rosner_89,
 author       = {Amir Pnueli and Roni Rosner},
 year         = {1989},
 title        = {On the Synthesis of a Reactive Module},
 booktitle    = {POPL},
 address      = {Austin, Texas, USA},
 pages        = {179--190},
 doi          = {10.1145/75277.75293},
)
@article(Raskin_CDH_07,
 author       = {Jean{-}Fran{\c{c}}ois Raskin and Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger},
 year         = {2007},
 title        = {Algorithms for Omega-Regular Games with Imperfect Information},
 journal      = {Logical Methods in Computer Science},
 volume       = {3},
 number       = {3},
 doi          = {10.2168/LMCS-3(3:4)2007},
)
@inproceedings(Renzelmann_Swift_09,
 author       = {Matthew J. Renzelmann and Michael M. Swift},
 year         = {2009},
 title        = {{Decaf}: Moving Device Drivers to a Moderm Language},
 booktitle    = {USENIX Annual Technical Conference},
 address      = {San Diego, CA, USA},
)
@inproceedings(Rudell_1993,
 author       = {Richard Rudell},
 year         = {1993},
 title        = {Dynamic variable ordering for ordered binary decision diagrams},
 booktitle    = {ICCAD},
 address      = {Santa Clara, CA, USA},
 pages        = {42--47},
 doi          = {10.1007/978-1-4615-0292-0\_5},
)
@misc(tsl,
 author       = {Leonid Ryzhyk},
 year         = {2014},
 title        = {{TSL2} Reference Manual},
)
@inproceedings(Ryzhyk_CKSH_09,
 author       = {Leonid Ryzhyk and Peter Chubb and Ihor Kuz and Le Sueur, Etienne and Gernot Heiser},
 year         = {2009},
 title        = {Automatic Device Driver Synthesis with {Termite}},
 booktitle    = {22nd ACM Symposium on Operating Systems Principles},
 address      = {Big Sky, MT, USA},
 doi          = {10.1145/1629575.1629583},
)
@inproceedings(Ryzhyk_KMRVH_11,
 author       = {Leonid Ryzhyk and John Keys and Balachandra Mirla and Arun Raghunath and Mona Vij and Gernot Heiser},
 year         = {2011},
 title        = {Improved Device Driver Reliability Through Hardware Verification Reuse},
 booktitle    = {16th International Conference on Architectural Support for Programming Languages and Operating Systems},
 address      = {Newport Beach, CA, USA},
 doi          = {10.1145/1950365.1950383},
)
@inproceedings(Ryzhyk_WKLRSV_14,
 author       = {Leonid Ryzhyk and Adam Walker and John Keys and Alexander Legg and Arun Raghunath and Michael Stumm and Mona Vij},
 year         = {2014},
 title        = {User-Guided Device Driver Synthesis},
 booktitle    = {OSDI},
 address      = {Broomfield, CO, USA},
)
@book(Sipser_96,
 author       = {Michael Sipser},
 year         = {1996},
 title        = {Introduction to the Theory of Computation},
 edition      = {1st},
 publisher    = {International Thomson Publishing},
 doi          = {10.1145/230514.571645},
)
@inproceedings(Solar-Lezama_RBE_05,
 author       = {Solar-Lezama, Armando and Rodric Rabbah and Bod\'{\i}k, Rastislav and Ebcio\u{g}lu, Kemal},
 year         = {2005},
 title        = {Programming by Sketching for Bit-streaming Programs},
 booktitle    = {PLDI},
 address      = {Chicago, Illinois, USA},
 doi          = {10.1145/1064978.1065045},
)
@inproceedings(Spear_RHHL_06,
 author       = {Michael F. Spear and Tom Roeder and Orion Hodson and Galen C. Hunt and Steven Levi},
 year         = {2006},
 title        = {Solving the starting problem: device drivers as self-describing artifacts},
 booktitle    = {1st EuroSys Conference},
 address      = {Leuven, Belgium},
 pages        = {45--57},
 doi          = {10.1145/1217935.1217941},
)
@inproceedings(Swift_BL_03,
 author       = {Michael M. Swift and Brian N. Bershad and Henry M. Levy},
 year         = {2003},
 title        = {Improving the Reliability of Commodity Operating Systems},
 booktitle    = {19th ACM Symposium on Operating Systems Principles},
 address      = {Bolton Landing (Lake George), New York, USA},
 doi          = {10.1145/1165389.945466},
)
@misc(vp,
 author       = {{Synopsys}},
 title        = {Virtual Prototyping Models},
 howpublished = {\url{http://www.synopsys.com/Systems/VirtualPrototyping/VPModels}},
)
@inproceedings(Thomas_95,
 author       = {Wolfgang Thomas},
 year         = {1995},
 title        = {On the Synthesis of Strategies in Infinite Games},
 booktitle    = {12th Annual Symposium on Theoretical Aspects of Computer Science},
 pages        = {1--13},
 doi          = {10.1007/3-540-59042-0\_57},
)
@misc(ddgen,
 author       = {{Vayavya Labs}},
 title        = {{Device Driver Generator tool}},
 howpublished = {\url{http://vayavyalabs.com/products/}},
)
@inproceedings(Walker_Ryzhyk_14,
 author       = {Adam Walker and Leonid Ryzhyk},
 year         = {2014},
 title        = {Predicate Abstraction for Reactive Synthesis},
 booktitle    = {FMCAD},
 address      = {Lausanne, Switzerland},
 doi          = {10.1109/FMCAD.2014.6987617},
)
@misc(dml,
 author       = {{Wind River}},
 year         = {2010},
 title        = {{Wind River Simics Model Builder} reference manual. Version 4.4},
)
@misc(dml_ug,
 author       = {{Wind River}},
 year         = {2010},
 title        = {{Wind River Simics Model Builder} user guide. Version 4.4},
)
@misc(ds12887,
 title        = {{WindRiver Simics DS12887 Model}},
 howpublished = {\url{http://www.windriver.com/products/simics}},
)
@misc(Yavatkar_12,
 author       = {Raj Yavatkar},
 year         = {2012},
 title        = {Era of {SoCs}, presentation at the {Intel Workshop on Device Driver Reliability, Modeling and Synthesis}},
)
@inproceedings(Zhou_CABE_06,
 author       = {Feng Zhou and Jeremy Condit and Zachary Anderson and Ilya Bagrak and Rob Ennals and Matthew Harren and George Necula and Eric Brewer},
 year         = {2006},
 title        = {{SafeDrive}: Safe and Recoverable Extensions Using Language-Based Techniques},
 booktitle    = {7th USENIX Symposium on Operating Systems Design and Implementation},
 address      = {Seattle, WA, USA},
 pages        = {45--60},
)