Systems code is ubiquitous and complex. Moreover, the complexity of code is expected to increase as systems designers can no longer expect increasing processor speeds, and thus must turn to concurrency for improved performance. How can we be sure that these programs, running on platforms ranging from human implant devices to nuclear power plant controls, will behave as intended? Addressing systems code correctness in the face of concurrency involves advances in two intertwined fields: automatic software verification and concurrent programming paradigms. In this talk I will discuss some of our recent work on improving both the correctness as well as the performance of systems software. I will focus primarily on describing a new automatic method of temporal logic verification of programs (POPL'11, CAV'11). I will also discuss recent results on a new language feature that has enabled more concurrency in transactional memory systems, improving performance by an order of magnitude (POPL'10, PPoPP'08, SPAA'08).
Eric Koskinen's research is centered around developing mathematical techniques which improve the safety and performance of software, and applying those techniques to realistic computer systems. He is currently a PhD candidate at the University of Cambridge, under the supervision of Dr. Byron Cook and Prof. Michael Gordon. Eric was awarded the Gates Cambridge Scholarship, completed an Sc.M from Brown University where he worked with Maurice Herlihy, interned thrice at Microsoft Research, and previously spent three years as a software engineer at Amazon.com.