Nicholas V. Lewchenko

<nicholas.lewchenko@colorado.edu>

I am a computer science PhD student at the University of Colorado Boulder, advised by Gowtham Kaki.

I am interested in the application of programming languages to distributed systems. My aim in this area is to identify programming model restrictions that make distributed programs easier to write, verify, and think about.

Publications

Bolt-On Strong Consistency: Specification, Implementation, and Verification Nicholas V. Lewchenko, Gowtham Kaki, Bor-Yuh Evan Chang,

Published in OOPSLA '25. [DOI] [talk]
RunTime-Assisted Convergence in Replicated Data Types Gowtham Kaki, Prasanth Prahladan, Nicholas V. Lewchenko.

Published in PLDI '22. [DOI]
Sequential Programming for Replicated Data Stores Nicholas V. Lewchenko, Arjun Radhakrishna, Akash Gaonkar, Pavol Černý.

Published in ICFP '19. [DOI] [slides]
DroidStar: Callback Typestates for Android Classes. Arjun Radhakrishna, Nicholas V. Lewchenko, Shawn Meier, Sergio Mover, Krishna Chaitanya Sripada, Damien Zufferey, Bor-Yuh Evan Chang, Pavol Černý.

Published in ICSE '18. [arXiv] [DOI] [slides]

Projects

Decidable Verification for Replication Systems (current)

The current focus is the verification of distributed consensus protocols, aiming to reduce the manual verification effort that is required by existing approaches. If you're interested check out my OOPSLA'25 talk on Bolt-On Strong Consistency: Specification, Implementation, and Verification.

To support this work, I have developed a program verification tool for Rust called Ravencheck.

Semantic Consistency Mechanisms for Replicated State Applications

The aim of this project is to design language abstractions for consistency configuration that are finer-grained than the typical Strong/Eventual choice, using datatype semantics to allow concurrency in more situations.

The major contribution is Carol, a programming language that makes the expression of a replicated operation's coordination requirements simple and efficient.

Sequential Programming for Replicated Data Stores Nicholas V. Lewchenko, Arjun Radhakrishna, Akash Gaonkar, Pavol Černý.

Published in ICFP '19. [DOI] [slides]
Discard, a Haskell library implementing the Carol language and runtime.

Active learning for asynchronous typestates

This project extended active learning techniques to systems with asynchronous behavior. The major contribution is DroidStar, a testing library for automatically generating "callback typestates" that specify callback-based Android classes.

DroidStar: Callback Typestates for Android Classes. Arjun Radhakrishna, Nicholas V. Lewchenko, Shawn Meier, Sergio Mover, Krishna Chaitanya Sripada, Damien Zufferey, Bor-Yuh Evan Chang, Pavol Černý.

Published in ICSE '18. [paper] [acm] [slides]
Abstract and poster which I presented for the SPLASH '17 Student Research Competition.