[portrait]

Christian J. Bell

My broad research interests are in how machine checked, modular, formal specifications can be used to improve the scalability and reliability of large software systems. A key piece of this puzzle is how to modularly specify concurrent imperative programs, and thus I am actively studying program logics and machine-checked proofs for verification of fine-grained concurrent programs. In the past, I have also worked on verifying loop-parallelizing compiler optimizations.