Bill Harris

Principal Scientist

My work develops verifiers that prove deep properties of program correctness or synthesize programs that are correct and secure by construction.



Before joining Galois, Bill was an Assistant Professor in the School of Computer Science at the Georgia Institute of Technology. There, he oversaw the Trustable Programming Group, which developed automatic program verifiers that prove properties about program performance, information leakage, and that prove functional equivalence of multiple programs.

Bill earned his Ph.D. in Computer Science from the University of Wisconsin-Madison, where he was advised by Thomas Reps and Somesh Jha. His thesis work developed a program synthesizer that instumented programs to be correct and secure when executed in environments that provide API’s for enforcing application security.

Journal Publications

William R. Harris, Sanjit Seshia, Somesh Jha, and Thomas Reps. Program Synthesis for Interactive-Security Systems. In Formal Methods in System Design (FMSD).

Selected Conference Publications
  • Ren Ding, Chenxiong Qian, Chengyu Song, William R. Harris, Taesoo Kim, and Wenke Lee. Efficient Protection of Path-sensitive Control Security. In the proceedings of the USENIX Security Symposium 2017.
  • Hyouk Jun Kwon, William R. Harris, and Hadi Esmaeilzadeh. Proving Flow Security of Sequential Logic via Automatically Synthesized Relational Invariants. In the proceedings of Computer Security Foundations (CSF) 2017.
  • Akhilesh Srikanth, Burak Sahin, and William R. Harris. Complexity Verification Using Guided Theorem Enumeration. Principles of Programming Languages (POPL) 2017.
  • Chengyu Song, Byoungyoung Lee, Kangjie Lu, William R. Harris, Taesoo Kim, and Wenke Lee. Enforcing Kernel Security Invariants with Data Flow Integrity. In the proceedings of the Network and Distributed System Security (NDSS) Symposium 2016.
  • Jongse Park, Hadi Esmaeilzadeh, Xin Zhang, Mayur Naik and William Harris. FlexJava: Language Support for Safe and Modular Approximate Programming. The European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE) 2015.
  • William R. Harris, Guoliang Jin, Shan Lu, and Somesh Jha. Validating Library Usage Interactively. In Computer Aided Verification (CAV) 2013.
  • William R. Harris, Somesh Jha, Thomas Reps, Jonathan Anderson, Robert N. M. Watson. Declarative, Temporal, and Practical Programming with Capabilities. In IEEE Symposium on Security and Privacy (Oakland) 2013.
  • William R. Harris, Somesh Jha, and Thomas Reps. Secure Programming via Visibly Pushdown Safety Games. In Computed Aided Verification (CAV) 2012.
  • William R. Harris and Sumit Gulwani. Spreadsheet Table Transformations from Examples. In Programming Language Design and Implementation (PLDI) 2011. This work was recognized in conjunction with Automating String Processing in Spreadsheets Using Input-Ouput Examples (Sumit Gulwani, POPL 2011) as a CACM Research Highlight.
  • William R. Harris, Somesh Jha, and Thomas Reps. DIFC Programs by Automatic Instrumentation. In Computer and Communications Security (CCS) 2010.
  • William R. Harris, Akash Lal, Aditya V. Nori, and Sriram K. Rajamani. Alternation for Termination. In Static Analysis Symposium (SAS) 2010.
  • William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta. Program Analysis via Satisfiability Modulo Path Programs. In Principles of Programming Languages (POPL) 2010.
  • William R. Harris, Nicholas A. Kidd, Sagar Chaki, Somesh Jha, and Thomas W. Reps. Verifying Information Flow Control over Unbounded Processes. In Formal Methods (FM) 2009.