References

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