|
Research
Modern programs are complex and, as a
result, often untrustworthy (i.e. incorrect or insecure). My work builds on recent advances in the development of secure systems to provide techniques for automatically synthesizing correct, secure programs.
Publications
My
entry on DBLP.
- 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)
Selected Technical Reports
- William R. Harris, Somesh Jha, Thomas Reps, Jonathan Anderson, Robert N. M. Watson. Declarative, Temporal, and Practical Programming with Capabilities. University of Wisiconsin-Madison TR1785
- William R. Harris, Somesh Jha, and Thomas Reps. Secure Programming via Visibly-Pushdown Safety Games. University of Wisconsin-Madison TR1710
- William R. Harris, Somesh Jha, and Thomas Reps. DIFC
Programs by Automatic Instrumentation. University of Wisconsin-Madison TR1673
|
