May 2017: David Heath will present Trustable, Locked, Reconfigurable Logic at TECHCON 2017
May 2017: Efficient Protection of Path-Sensitive Control Security will be published in the proceedings of USENIX Security 2017
April 2017: I will be serving on the PC for IEEE SecDev
April 2017: I will be serving on the PC for APLAS 2017
April 2017: Proving Flow Security of Sequential Logic via Automatically Synthesized Relational Invariants will be published in the proceedings of CSF 2017
April 2017: Burak Sahin will join the group as a PhD student.
April 2017: David Heath received the CS 7001 Research Project Award
April 2017: Akhilesh Srikanth received the Donald V. Jackson Fellowship
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. In Design, Automation, and Test in Europe (DATE) 2013.
Sumit Gulwani, William R. Harris, and Rishabh Singh. Spreadsheet Data Manipulation Using Examples. In Commun. ACM (CACM) 55(8) (2012).
Refereed papers
William R. Harris, Sanjit Seshia, Somesh Jha, and Thomas Reps. krogram Synthesis for Interactive-Security Systems To appear in the proceedings of FMCAD 2017.
Ren Ding, Chenxiong Qian, Chengyu Song, William R. Harris, Taesoo Kim, and Wenke Lee. Efficient Protection of Path-sensitive Control Security. To appear 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
. To appear in the proceedings of Computer Security Foundations (CSF) 2017. (preprint: pdf)
Akhilesh Srikanth, Burak Sahin, and William R. Harris. Complexity Verification Using Guided Theorem Enumeration. Principles of Programming Languages (POPL) 2017. (preprint: pdf)
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. (preprint: pdf)
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. (preprint: pdf)
William R. Harris, Guoliang Jin, Shan Lu, and Somesh Jha. Validating Library Usage Interactively. In Computer Aided Verification (CAV) 2013. (preprint: 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)
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)
William R. Harris and Sumit Gulwani. Spreadsheet Table
Transformations from Examples. In Programming Language Design
and Implementation (PLDI)
2011. (preprint: pdf). 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. (preprint: pdf)
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.
(preprint: pdf)
William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, and
Aarti Gupta. Program Analysis via Satisfiability Modulo Path
Programs. In Principles of Programming
Languages (POPL)
2010. (preprint: pdf)
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.
(preprint: pdf)
Talks
Secure Programming via Game-based Synthesis.
National University of Singapore School of Computing Colloqium.
Singapore.
24 April 2014.
Secure Programming via Game-based Synthesis.
University of California, Los Angeles Dept. of Computer Science Colloqium.
Los Angeles, CA, USA. 21 April 2014.
Secure Programming via Game-based Synthesis.
University of Toronto Dept. of Computer Science Colloqium.
15 April 2014.
Secure Programming via Game-based Synthesis.
Georgia Institute of Technology School of Computer Science Colloqium.
Atlanta, GA, USA.
8 April 2014.
Secure Programming via Game-based Synthesis.
North Carolina State Dept. of Computer Science Colloqium.
31 March 2014.
Raleigh, NC, USA.
Secure Programming via Game-based Synthesis.
University of Pittsburgh Dept. of Computer Science.
28 March 2014.
Pittsburgh, PA, USA.
Secure Programming via Game-based Synthesis.
Purdue University Dept. of Computer Science Colloqium.
25 March 2014.
West Lafayette, IN, USA.
Secure Programming via Game-based Synthesis.
Ohio State University Dept. of Computer Science Colloqium.
20 March 2014.
Columbus, OH, USA.
Secure Programming via Game-based Synthesis.
University of Rochester Dept. of Computer Science Colloqium.
14 March 2014.
Rochester, NY, USA.
Secure Programming via Game-based Synthesis.
SUNY Stony Brook Dept. of Computer Science Colloqium.
Stony Brook, NY, USA.
27 Feb 2014.
Secure Programming via Game-based Synthesis.
College of William and Mary Dept. of Computer Science Colloqium.
Williamsburg, VA, USA.
25 Feb 2014.
Secure Programming via Game-based Synthesis.
University of Iowa Dept. of Computer Science Colloqium.
Iowa City, IA, USA.
19 Feb 2014.
Secure Programming via Game-based Synthesis.
University College London Dept. of Computer Science Colloqium.
London, UK.
21 Jan 2014.
Secure Programs via Game-based Synthesis. At Formal Methods in Computer-Aided Design (FMCAD) 2013. Portland, OR, USA. (slides: Keynote (native format),
PPT,
PDF)
Validating Library Usage Interactively. At Computer Aided Verification (CAV) 2013, St. Petersburg, RU. (slides: Keynote (format), PPT, PDF)
Declarative, Temporal, and Practical Programming with Capabilities
IEEE Symposium on Security and Privacy (Oakland) 2013, San Francisco, CA, USA (slides: Keynote (native format), PPT, PDF)
Secure Programming via Visibly Pushdown Safety Games.
Google Inc., Madison, WI, USA
Secure Programming via Visibly Pushdown Safety Games.
Computer Aided Verification (CAV) 2012, Berkeley, CA, USA (slides: PPTX)
Spreadsheet Table Transformations from Examples.
Programming Language Design and Implementation (PLDI) 2011, San Jose, California, USA. (slides: PPTX)
Policy Weaving for Secure Systems, MIT Programming Languages Working Group Massachusetts Institute of Technology, Boston, MA, USA
DIFC Programs by Automatic Instrumentation. Computer and Communications Security (CCS) 2010, Chicago, Illinois, USA. (slides: PPTX)
Alternation for Termination. Static Analysis Symposium (SAS) 2010, Perpignan, France. (slides: PPTX)
Program Analysis via Satisfiability Modulo Path Programs. Principles of Programming Languages (POPL) 2010, Madrid, Spain. (slides: PPT)
Verifying Information Flow Control Over Unbounded Processes.
Formal Methods (FM) 2009, Eindhoven, North Brabant, Netherlands. (slides: PPTX)
Teaching
Fall 2016: CS 4392: Programming Languages
Spring 2016, Spring 2017: CS 4240: Compilers and Interpreters
The layout of this site is (pretty obviously) based directly on webpages designed and developed by Prof. Matt Might. If you are interested in using the layout for your own purposes, please contact him to request permission.