Santiago joined Galois as a Research Engineer in 2020. At Galois, Santiago applies his deep knowledge and interest in formal methods, separation logic, software safety, machine-checked proofs, and compilers to the projects he works on. Santiago’s most recent work focused on modular verification of realistic compilers for concurrent programs. He has also worked on logics for program verification, with an emphasis on Concurrent Separation Logic.
Prior to Galois, Santiago earned his M.A. and Ph.D. in Computer Science from Princeton University, and a Bachelors in Mathematics from MIT. His academic work focused on programming languages and compiler correctness for concurrency. His dissertation explored modular proofs of optimizing compilers with shared memory concurrency.