David is Adjunct Assistant Professor at the University of Vermont and Principal Scientist at Galois, Inc., an R&D lab that specializes in secure software development. David builds new programming languages and analysis tools that help programmers build reliable software for security-sensitive and privacy-sensitive applications. In particular, David's tools focus on symbolic software analysis methods to prove the absence of entire classes of defects, i.e., not just fixing the next bug, but showing the absence of the last bug.
Adjunct Assistant Professor, Computer Science
Publications
Zero Knowledge Static Program Analysis. Zhiyong Fang, David Darais, Joe Near, Yupeng Zhang. To appear in Computer and Communications Security (CCS). ACM, 2021.
A Language for Probabilistically Oblivious Computation. David Darais, Ian Sweet, Chang Liu, Michael Hicks. Principles of Programming Languages (POPL). ACM, 2020.
Proof Carrying Network Code. Christian Skalka, John Ring, David Darais, Minseok Kwon, Sahil Gupta, Kyle Diller, Steffan Smolka, Nate Foster. Computer and Communications Security (CCS). ACM, 2019.
Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy. Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, Dawn Song. Object-oriented Programming, Systems, Languages, and Applications (OOPSLA). ACM, 2019. ACM SIGPLAN Distinguished Paper Award.
Abstracting Definitional Interpreters. David Darais, Nicholas Labich, Phúc C. Nguyễn, David Van Horn. International Conference on Functional Programming (ICFP). ACM, 2017.
Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis. David Darais, Matthew Might, David Van Horn. Object-Oriented Programming, Systems, Languages & Applications (OOPSLA). ACM, 2015.
Functional Pearl: Parsing with Derivatives. Matthew Might, David Darais, Daniel Spiewak. International Conference on Functional Programming (ICFP). ACM, 2011.
Areas of Expertise and/or Research
Programming analysis, mechanized proofs, software defined networking, differential privacy, secure multiparty computation
Education
- University of Utah, B.S.
- Harvard University, M.S.
- University of Maryland, Ph.D.
Contact
Email:
Website(s):
Courses Taught
- UVM CS 225: Programming Languages / Spring 2020
- UVM CS 295A: Software Verification / Fall 2019
- UVM CS 225: Programming Languages / Spring 2019
- UVM CS 295A: Software Verification / Fall 2018
- UVM CS 225: Programming Languages / Spring 2018