photo  

Leonid Ryzhyk

Senior Researcher,
VMware Research
CV

Contact Information

Physical: 665 Clyde Ave
Mountain View, CA 94043
USA
E-mail: leonid@ryzhyk.net
GPG key Fingerprint: F065 3B03 1724 6C55 34F1 666B 1194 50D9 FD27 C23E
Phone: +1 412 425 2100

Research

Before joining VMware, I got my PhD from the University of New South Wales and NICTA, worked as researcher at NICTA (2009-2013), a postdoc at the University of Toronto (2013-2014) and at the Carnegie Mellon University (2014-2015), and a researcher at Samsung Research America. The main theme of my work is applying formal methods to build better operating systems and networks.

I have worked on the following projects:

  • Cocoon: Correct by construction networking
  • Termite: Automatic device driver synthesis
  • Liss: Synchronization synthesis for systems code
  • Bilby: Automatic verification and synthesis of file systems
  • Dingo: A reliable device driver framework

Conference and journal publications

Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, and George Varghese Correct by Construction Networks using Stepwise Refinement [PDF] NSDI'17
Pavol Cerny, Edmund Clarke, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis [PDF] FMSD'16
Alexander Legg, Nina Narodytska, Leonid Ryzhyk A SAT-Based Counterexample Guided Method for Unbounded Synthesis [PDF] CAV'16
Pavol Cerny, Edmund Clarke, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis [PDF][Technical report] CAV'15
Niklas Een, Alexander Legg, Nina Narodytska, and Leonid Ryzhyk SAT-based Strategy Extraction in Reachability Games [PDF] AAAI'15
Leonid Ryzhyk, Adam Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm, and Mona Vij User-Guided Device Driver Synthesis [PDF] OSDI'14
Adam Walker and Leonid Ryzhyk Predicate Abstraction for Reactive Synthesis [PDF][Technical report] FMCAD'14
Pavol Cerny, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach Regression-Free Synthesis for Concurrency [PDF] CAV'14
Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk, and Adam Walker Solving Games without Controllable Predecessor [PDF] CAV'14
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu Automatic Verification of Active Device Drivers ACM SIGOPS Operating Systems Review, Volume 48 Issue 1, January 2014 [PDF] OSR
Mona Vij, John Keys, Arun Raghunath, Scott Hahn, Vincent Zimmer, Leonid Ryzhyk, Adam Walker and Alexander Legg Device Driver Synthesis Intel Technology Journal, Volume 17, Issue 2 December 2013 [PDF] Intel Tech J
Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach Efficient Synthesis for Concurrency using Semantics-Preserving Transformations [PDF] CAV'13
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu Automatic Verification of Message-Based Device Drivers [PDF] SSV'12
Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser Improved Device Driver Reliability through Hardware Verification Reuse [PDF] ASPLOS'11
Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser Automatic Device Driver Synthesis with Termite [PDF] SOSP'09,
Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser Dingo: Taming Device Drivers [PDF] EuroSys'09,

Other publications

Abhiram Balasubramanian, Marek S. Baranowski, Anton Burtsev, Aurojit Panda, Zvonimir Rakamarić, Leonid Ryzhyk System Programming in Rust: Beyond Safety [PDF] HotOS'17
Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Nina Narodytska, Cole Schlesinger, Douglas B. Terry, and George Varghese Towards Correct-by-Construction SDN [PDF] NetPL'16
Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker The Third Reactive Synthesis Competition (SYNTCOMP 2016) [PDF] SYNTCOMP'16
Leonid Ryzhyk, Adam Walker Developing a Practical Reactive Synthesis Tool: Experience and Lessons Learned [PDF] SYNT'16
Swen Jacobs, Roderick Bloem, Romain Brenguier, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, and Adam Walker The Second Reactive Synthesis Competition (SYNTCOMP 2015) [PDF] SYNTCOMP'15
Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, and Adam Walker The First Reactive Synthesis Competition (SYNTCOMP 2014) [PDF] SYNTCOMP 2014
Gabi Keller, Toby Murray, Sidney Amani, Liam O'Connor-Davis, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser File systems deserve verification too! [PDF] PLOS'13
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu Active Device Drivers [PDF] NICTA TR
Sidney Amani, Leonid Ryzhyk, Alastair Donaldson, Gernot Heiser, Alexander Legg and Yanjin Zhu Static analysis of device drivers: we can do better! ApSys'11
Gernot Heiser, Leonid Ryzhyk, Michael von Tessin, Aleksander Budzynowski What if you could actually Trust your kernel? [PDF] HotOS'11
Leonid Ryzhyk On the Construction of Reliable Device Drivers [PDF] PhD thesis,
Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk The Road to Trustworthy Systems [PDF] STC'10
Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser Improved Device Driver Reliability through Verification Reuse [PDF] HotDep'10
Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser The Case for Active Device Drivers [PDF] ApSys'10
Leonid Ryzhyk, Ihor Kuz and Gernot Heiser Formalising device driver interfaces [PDF] PLOS'07,
Leonid Ryzhyk, Timothy Bourke and Ihor Kuz Reliable device drivers require well-defined protocols [PDF] HotDep'07,
Leonid Ryzhyk and Ihor Kuz Towards operating system support for application-specific fault-tolerance protocols [PDF] WOSSA'06