Job Application
Research Summary
Modern programs are complex and, as a result, often untrustworthy
(i.e. incorrect or insecure). In princi- ple, modern research in
programming languages provides powerful techniques for verifying and
synthesizing correct programs, but in practice, such techniques have
subtle limitations. My research extends and applies such techniques to
enable programmers to build practical, trustworthy programs.
Application Materials
Publications
- William R. Harris, Guoliang Jin, Shan Lu, and Somesh Jha. Validating Library Usage Interactively. In Computer Aided Verification (CAV) 2013. (preprint: pdf, talk: Keynote, PPT, PDF)
- 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. (preprint: pdf, talk: Keynote, PPT, PDF)
-
Florian Sagstetter, Martin Lukasiewycz, Sebastian Steinhorst, Marko Wolf, Alexandre Bouard, William R. Harris, Somesh Jha, Thomas Peyrin, Axel Poschmann, Samarjit Chakraborty. Security Challenges in Automotive Hardware / Software Architecture Design. To appear in Design, Automation, and Test in Europe (DATE) 2013.
- William R. Harris, Somesh Jha, and Thomas Reps. Secure
Programming via Visibly Pushdown Safety Games.
In Computed Aided Verification (CAV) 2012. The original
publication is available
at www.springerlink.com.
(pdf | slides)
- Sumit Gulwani, William R. Harris, and Rishabh
Singh. Spreadsheet Data Manipulation Using Examples.
In Commun. ACM (CACM) 55(8) (2012).
- William R. Harris and Sumit Gulwani. Spreadsheet Table
Transformations from Examples. In Programming Language Design
and Implementation (PLDI)
2011. (pdf | slides). 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. (pdf
| slides)
- William R. Harris, Akash Lal, Aditya V. Nori, and Sriram
K. Rajamani. Alternation for Termination. In
Static Analysis Symposium (SAS) 2010. The original publication
is available
at www.springerlink.com.
(pdf |
slides)
- William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, and
Aarti Gupta. Program Analysis via Satisfiability Modulo Path
Programs. In Principles of Programming
Languages (POPL)
2010. (pdf
| slides)
- 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. The
original publication is available
at www.springerlink.com.
(pdf
| slides)
|