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.
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.
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.
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.
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.
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.
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.
Roderick Bloem, Robert Könighofer & Martina Seidl (2013):
SAT-Based Synthesis Methods for Safety Specs.
CoRR abs/1311.3530.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Rayna Dimitrova & Bernd Finkbeiner (2008):
Abstraction Refinement for Games with Incomplete Information.
In: FSTTCS,
Bangalore, India.
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.
Rüdiger Ehlers, Robert Könighofer & Georg Hofferek (2012):
Symbolically synthesizing small circuits.
In: FMCAD,
Cambridge, UK,
pp. 91–100.
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.
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.
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.
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.
Swen Jacobs (2014):
Extended AIGER Format for Synthesis.
CoRR abs/1405.5793.
Barbara Jobstmann & Roderick Bloem (2006):
Optimizations for LTL Synthesis.
In: FMCAD,
San Jose, CA, USA,
pp. 117–124,
doi:10.1109/fmcad.2006.22.
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.
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.
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.
Etienne Kneuss, Viktor Kuncak, Ivan Kuraj & Philippe Suter (2013):
On Integrating Deductive Synthesis and Verification Systems.
CoRR abs/1304.5661.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Matthew J. Renzelmann & Michael M. Swift (2009):
Decaf: Moving Device Drivers to a Moderm Language.
In: USENIX Annual Technical Conference,
San Diego, CA, USA.
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.
Leonid Ryzhyk (2014):
TSL2 Reference Manual.
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.
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.
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.
Michael Sipser (1996):
Introduction to the Theory of Computation,
1st edition.
International Thomson Publishing,
doi:10.1145/230514.571645.
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.
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.
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.
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.
Raj Yavatkar (2012):
Era of SoCs, presentation at the Intel Workshop on Device Driver Reliability, Modeling and Synthesis.
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.