I am an applied scientist in the Automated Reasoning Group at Amazon Web Services.  My research focuses on language-based modeling and verification of software systems and networks.


I received a Ph.D. from Princeton University in 2015, advised by David Walker.





JavaScript has emerged as the de facto language of the web and is gaining traction for programming apps, wearables, and even embedded microcontrollers. But executing JavaScript quickly with just-in-time compilation is memory-intensive, while interpreters are memory-efficient but slow.


The SJSx project aggressively reduces the memory footprint of JavaScript execution via type-directed ahead-of-time compilation while achieving performance competitive to modern just-in-time compilers. Along the way, we developed a novel type inference algorithm for a type system with objects, structural subtyping, prototype inheritance, and first-class methods.


People. Satish Chandra, Colin Goron, Jean-Baptiste Jeannin, Manu Sridharan, Frank Tip, Youngil Choi.


Papers. OOPSLA 2016.




Many modern languages have support for automatic type inference. But when inference fails, the error messages reported can be opaque, highlighting a code location far from the source of the problem.


The Hobbes project provides a framework for extending existing type inference algorithms to produce error reports based on correcting sets, which contain a minimal set of type constraints that, if fixed, allow the program to type check. By leveraging the existing type inference algorithm, Hobbes gains a substantial performance boost compared to other error reporting engines, and adoption is much simpler.



People. Satish Chandra, Calvin Loncaric, Manu Sridharan.


Papers. OOPSLA 2016.

Verified SDN



Software-defined networking promises rapid innovation and efficient deployment by shifting intelligence from switching hardware to software on a logically-centralized server. But software development is notoriously error-prone, and bugs in SDN controller software can cause network vulnerabilities.


The Cocoon project provides a simple, declarative specification language for packet-forwarding properties embedded in a richer language for network design. Cocoon translates controller programs to Boogie and automatically checks whether a program satisifies its specification.


People. Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Nina Narodytska, Cole Schlesinger, Douglas B. Terry, and George Varghese.


Papers. NetPL 2016.

Theory of reprogrammable

packet-processing pipelines


In a Software-Defined Network (SDN), a central, computationally powerful controller manages a set of distributed, computationally simple switches. The controller computes a policy describing how each switch should route packets, and it then populates packet-processing tables on each switch with rules to enact the routing policy. As network conditions change, the controller continues to add and remove rules from switches to adjust the policy as needed.


The CNC project develops a language for targeting reconfigurable packet-processing hardware and a proved-correct compiler for compiling a virtual pipeline to heterogeneous back-end hardware. It builds on the NetKAT language to provide a sound equational theory for program transformations.


People. Carolyn Anderson, Nate Foster, Arjun Guha, Michael Greenberg, Jean-Baptiste Jeannin, Dexter Kozen, David Walker.


Papers. POPL 2014, ICFP 2014, Dissertation.


p4v: Practical Verification for Programmable Data Planes. Jed Liu, William Hallahan, Cole Schlesinger, Milad Sharif, Jeongkeun Lee, Robert Soulé, Han Wang, Călin Cascaval, Nick McKeown, and Nate Foster.  SIGCOMM 2018.



Iota: A Calculus for Internet of Things Automation. Julie L. Newcomb, Satish Chandra, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan. Onward! 2017.



Correct by Construction Networks Using Stepwise Refinement.  Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, and George Varghese.  NSDI 2017.



Type Inference for Static Compilation of JavaScript.  Satish Chandra, Colin Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan, Frank Tip, Yong-Il Choi. OOPSLA 2016.



A Practical Framework for Type Inference Error Explanation. Calvin Loncaric, Satish Chandra, Cole Schlesinger, Manu Sridharan. OOPSLA 2016.



Towards Correct-by-construction Network Programming.  Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Nina Narodytska, Cole Schlesinger, Douglas B. Terry, and George Varghese.  ACM SIGCOMM Workshop on Networking and Programming Languages.  August 2016.



Abstractions for Software-defined Networks. Cole Schlesinger. Ph.D. disstertation, June 2015.

[pdf, prototype]


Quality of Service Abstractions for Software-defined Networks. Cole Schlesinger, Hitesh Ballani, Thomas Karagiannis, Dimitrios Vytiniotis.  Technical Report.  March 2015.



Transparent, Live Migration of a Software-defined Network. Soudeh Ghorbani, Cole Schlesinger, Matthew Monaco, Eric Keller, Matthew Caesar, Jennifer Rexford, and David Walker. SOCC 2014.



Concurrent NetCore: From Policies to Pipelines. Cole Schlesinger, Michael Greenberg, and David Walker. ICFP 2014.



NetKAT: Semantic Foundations for Networks. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. POPL, 2014.



The Frenetic Network Controller. The Frenetic Contributors. The OCaml Users and Developers Workshop, 2013.


Towards JavaScript Verification with the Dijkstra State Monad. Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Ben Livshits. PLDI, 2013.



Languages for Software-defined Networks. Nate Foster, Arjun Guha, Mark Reitblatt, Alec Story, Michael J. Freedman, Naga Praveen Katta, Christopher Monsanto, Joshua Reich, Jennifer Rexford, Cole Schlesinger, David Walker, and Rob Harrison. IEEE Communications Magazine, Vol. 51, No. 2. February 2013.



Abstractions for Network Update. Mark Reitblatt, Nate Foster, Jen Rexford, Cole Schlesinger, and David Walker. SIGCOMM, August 2012.



Splendid Isolation: A Slice Abstraction for Software-Defined Networks. Stephen Gutz, Alec Story, Cole Schlesinger, Nate Foster. HotSDN, August 2012.



Modular Protections against Non-control Data Attacks. Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, and Benjamin Zorn. CSF, July 2011.

[pdf | tech report]

Research Interns

I occasionally have the opportunity to take on summer research interns. Please contact me if interested.




Andres Noetzli (Stanford University) on optimizations for improving the performance of "who can access my resource" analyses of AWS Identity and Access Management (IAM) policies.  Summer 2019.


Bernhard Gleiss (TU Wein) on optimizations for improving the scalability of Tiros, a service for verifying reachability properties of EC2 deployments.  Fall 2018.




William Hallahan (Yale University) on practical verification of P4 programs.  Summer 2017.




Julie Newcomb (University of Washington) on design and analysis of end-user automation for the Internet of Things. Summer 2016.


Calvin Loncaric (University of Washington) on a framework for improved error explanation for type inference. Summer 2015.


Last modified September, 2019.