Designing and maintaining networked systems poses many challenges to both developers and operators alike. Unexpected behavior can often result from subtle interactions between the networked entities and better tools are needed to help understand the underlying complexity. The stakes are also ever increasingly higher, as more and more of our lives depend on the reliable and correct operation of these networked systems.
In this talk I will show how techniques borrowed from the programming languages community can be used to facilitate the verification of networked systems, much like what has been done for monolithic systems and mission critical applications. The main focus of the talk will be on how these techniques were used to create the Protocol Interoperability Checker (PIC) to verify network protocol implementations. I will also describe my recent work on generalizing these verification techniques to handle more complex distributed systems and more expressive correctness semantics, while also discussing potential future applications. Finally, I will talk about my efforts towards verifying router configurations and keeping the resulting network policy consistent.
Luis Pedrosa is a PhD Candidate at the University of Southern California, where he is advised by Prof. Ramesh Govindan. His main lines of research lie at the intersection of the systems and programming languages communities and his work has made significant contributions to the field of networked systems verification. He has been inducted into the Phi Kappa Phi honor society and his work has been recognized with the USC Computer Science Department Best Research Assistant Award.
While Luis’ main research interests concern the novel applications of PL techniques towards the understanding and improvement of modern networked systems, he has also worked in a wide variety of other fields, including large-scale cluster management, mobile and cloud computing, low-power embedded systems, design automation, and even reverse engineering automotive electronic control units.