photo  

Leonid Ryzhyk

Postdoctoral Fellow,
Electrical and Computer Engineering Department
University of Toronto

Researcher (part-time),
Software Systems Research Group
National ICT Australia

Conjoint Lecturer,
School of Computer Science and Engineering,
University of New South Wales

CV

Contact Information

Physical: Office 463, Level 4
D.L. Pratt Building
6 King's College Road
University of Toronto
Toronto, Ont, M5S 3H5
Canada
E-mail: leonid.ryzhyk@utoronto.ca
GPG key Fingerprint: F065 3B03 1724 6C55 34F1 666B 1194 50D9 FD27 C23E
Phone: +1 416 562 1045

Research

The main theme of my research is applying formal methods to operating systems. I am particularly interested in applications that go beyond formal verification. For example, I investigate techniques for automatic and semi-automatic synthesis of correct-by-construction OS components.

I am currently working on three projects:

  • Termite: Automatic device driver synthesis
  • Dingo: A new device-driver architecture for improved reliability
  • Bilby: Automatic verification and synthesis of file systems

Publications

Leonid Ryzhyk, Adam Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm, and Mona Vij User-Guided Device Driver Synthesis OSDI'14 Broomfield, CO, USA, October 2014 [PDF]
Adam Walker and Leonid Ryzhyk Predicate Abstraction for Reactive Synthesis FMCAD'14 Lausanne, Switzerland, October 2014 [PDF][Technical report]
Pavol Cerny, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach Regression-Free Synthesis for Concurrency CAV'14 Vienna, Austria, July 2014 [PDF]
Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk, and Adam Walker Solving Games without Controllable Predecessor CAV'14 Vienna, Austria, July 2014 [PDF]
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]
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]
Gabi Keller, Toby Murray, Sidney Amani, Liam O'Connor-Davis, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser File systems deserve verification too! PLOS 2013 Nemacolin Woodlands Resort, Farmington, Pennsylvania, USA, Novemeber 2013 [PDF]
Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach Efficient Synthesis for Concurrency using Semantics-Preserving Transformations CAV 2013 Saint Petersburg, Russia, July 2013 [PDF]
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu Automatic Verification of Message-Based Device Drivers SSV 2012 Sydney, Australia, November 2012 [PDF]
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu Active Device Drivers NICTA Technical Report [PDF]
Sidney Amani, Leonid Ryzhyk, Alastair Donaldson, Gernot Heiser, Alexander Legg and Yanjin Zhu Static analysis of device drivers: we can do better! ApSys 2011 Shanghai, China
Gernot Heiser, Leonid Ryzhyk, Michael von Tessin, Aleksander Budzynowski What if you could actually Trust your kernel? HotOS 2011 Napa, CA, USA [PDF]
Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser Improved Device Driver Reliability through Hardware Verification Reuse ASPLOS 2011 Newport Beach, California, USA, March 2011 [PDF]
Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk The Road to Trustworthy Systems 5th Workshop on Scalable Trusted Computing, Chicago, IL, USA, October, 2010 [PDF]
Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser Improved Device Driver Reliability through Verification Reuse HotDep 2010, Vancouver, Canada, October, 2010 [PDF]
Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser The Case for Active Device Drivers ApSys 2010, New Delhi, India, August, 2010 [PDF]
Leonid Ryzhyk On the Construction of Reliable Device Drivers PhD thesis, Sydney, Australia, January, 2010 [PDF]
Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser Automatic Device Driver Synthesis with Termite SOSP 2009, Big Sky, MT, USA, October, 2009 [PDF]
Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser Dingo: Taming Device Drivers EuroSys 2009, Nuremberg, Germany, April, 2009 [PDF]
Leonid Ryzhyk, Ihor Kuz and Gernot Heiser Formalising device driver interfaces PLOS 2007, Stevenson, Washington, USA, October, 2007 [PDF]
Leonid Ryzhyk, Timothy Bourke and Ihor Kuz Reliable device drivers require well-defined protocols HotDep 2007, Edinburgh, UK, June, 2007 [PDF]
Leonid Ryzhyk and Ihor Kuz Towards operating system support for application-specific fault-tolerance protocols 2nd International Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January, 2006 [PDF]

Personal