R. Bocchino, E. Gamble, K. Gostelow, and R. Some.  Spot:  A Programming Language for Verified Flight Software, HILT 2014.
Ph.D. Thesis
This thesis was awarded the John C. Reynolds Doctoral Dissertation Award from ACM SIGPLAN and the David J. Kuck Outstanding Thesis Award from the University of Illinois.
Book Chapters
R. Bocchino, Alias Control for Deterministic Parallelism, in Dave Clarke, James Noble, and Tobias Wrigstad, editors, Aliasing in Object-Oriented Programming, Springer 2013 .