Assistant Professor
Computer Science
University of Vermont
Votey 319
David.Darais@uvm.edu
@daviddarais

@davdar

★ I am looking for PhD students to work with me in programming languages and/or computer security. I am also looking for motivated undergraduate and masters students to advise in research.
My research addresses problems in software reliability through advances in program analyzers, computer-checkable proofs of software correctness, and their combination.
I study techniques for achieving highly reliable software. Current methods for software reliability are either insufficient for critical software because they don't catch enough bugs, or they are too expensive to implement. My research considers the only known technique to give 100% assurance in software reliability—computer-checkable proofs, aka mechanized verification—and reduces the effort required to adopt these techniques.
I develop program analyzers which are fully automated tools for verifying the correctness of software. I then mechanically verify these program analyzers so their results can be trusted to achieve high assurance in critical settings. Finally, I design reusable components which can be used to build reliable program analyzers for new programming languages and analysis domains.
Abstracting Definitional Interpreters
I developed Abstracting Definitional Interpreters (w/Labich, Nguyễn and Van Horn), a framework for designing program analyzers from definitional interpreters. Using this framework, fragments of interpreters are used to construct new program analyzers, and these fragments are reusable across different programming languages. In addition to achieving compositional program analyzer construction, we show that pushdown precision of the analysis—a precise model for call-return matching—is achieved automatically from the setting of abstract definitional interpreters.
Constructive Galois Connections
I developed Constructive Galois Connections (w/Van Horn), which solves the open problem of mechanically verifying program analyzers using abstract interpretation, a theory of sound approximation for programs. Current approaches only support half of this theory in mechanized verification due to limitations in the underlying mathematics, and our insight is to design a new, related theory which simultaneously supports sound approximation and support for mechanized verification. This was done by looking to the parent framework for which abstract interpretation is one instance—called adjunctions—and re-instantiating this framework to support both sound approximation of programs and mechanized verification.
Galois Transformers
I developed Galois Transformers (w/Might and Van Horn), a compositional framework for building program analyzers. The framework contains building blocks for constructing analysers with varying precision, including path and flow sensitivity, and we prove that any composition of building blocks is guaranteed to be correct. Using this framework, variations in program analysis precision can be rapidly prototyped while maintaining the correctness of each prototype.
Teaching
- ⌁ UVM CS 225: Programming Languages / Spring 2019 ⌁
- UVM CS 295A: Software Verification / Fall 2018
- UVM CS 225: Programming Languages / Spring 2018
Publications
-
David Darais, Nicholas Labich, Phúc C. Nguyễn, David Van Horn.
Abstracting Definitional Interpreters.
International Conference on Functional Programming (ICFP). 2017. ACM.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
David Darais, David Van Horn.
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.
International Conference on Functional Programming (ICFP). 2016. ACM.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
David Darais, Matthew Might, David Van Horn.
Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis.
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA). 2015. ACM.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Ilya Sergey, Dominique Divriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens.
Monadic Abstract Interpreters.
Programming Language Design and Implementation (PLDI). 2013. ACM.
[pdf] [abstract] [bibtex] [ACM] -
Matthew Flatt, Ryan Culpepper, David Darais, Robert Bruce Findler.
Macros that Work Together: Compile-time bindings, partial expansion, and definition contexts.
Journal of Functional Programming (JFP). 2012. Cambridge University Press.
[pdf] [abstract] [bibtex] [ACM] -
Matthew Might, David Darais, Daniel Spiewak.
Functional Pearl: Parsing with Derivatives.
International Conference on Functional Programming (ICFP). 2011. ACM.
[pdf] [abstract] [bibtex] [ACM]
Theses
-
David Darais.
Mechanizing Abstract Interpretation.
PHD Thesis. University of Maryland. 2017.
[pdf] [abstract] [slides.pdf] [slides.key]
Workshops
-
David Darais.
Compositional and Mechanically Verified Program Analyzers.
ECOOP Doctoral Symposium (ECOOP-DS). 2016.
[pdf] [abstract] [slides.pdf] [slides.key]
Drafts
-
Joseph Near, David Darais, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel
Somani, Mu Zhang, Nikhil Sharma, Alex Shan, Dawn Song.
Duet: A Language and Type System for Statically Enforcing (ε,δ)-Differential Privacy
Draft. November 2018.
[pdf] [abstract] -
David Darais, Chang Liu, Ian Sweet, Michael Hicks.
A Language for Probabilistically Oblivious Computation.
Draft. July 2018.
[pdf] [abstract] -
Kristopher Micinski, David Darais, Thomas Gilray.
Abstracting Faceted Execution: Static Analysis of Dynamic Information-flow Control for Higher-order Languages.
Draft. July 2018.
[pdf] [abstract] -
David Darais, David Van Horn
Constructive Galois Connections (Extended Version)
Draft. March 2018.
[pdf] [abstract] -
David Christiansen, David Darais, Weixi Ma.
The Final Pretty Printer.
Draft. May 2017.
[pdf] [abstract]
Talks
-
A Simple and Extensible Approach to Program Analysis.
International Federation for Information Processing Working Group 2.4 on Software Implementation Technology (IFIP WG2.4). Essex, Vermont, USA. Oct, 2017.
[abstract] [slides.pdf] [slides.key] -
Abstracting Definitional Interpreters.
International Conference on Functional Programming (ICFP). Oxford, England. September, 2017.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.
International Conference on Functional Programming (ICFP). Nara, Japan. September, 2016.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Compositional and Mechanically Verified Program Analyzers.
ECOOP Doctoral Symposium (ECOOP-DS). Rome, Italy. July, 2016.
[pdf] [abstract] [slides.pdf] [slides.key] -
Constructive Galois Connections.
New Jersey Programming Languages and Systems Seminar (NJPLS). Philadelphia, Pennsylvania, USA. May, 2016.
[slides.pdf] [slides.key] -
Adventures in Abstract Interpretation.
Research Seminar. University of Utah. February, 2016.
[slides.pdf] [slides.key] [video] -
Constructive Galois Connections: With Applications to Abstracting Gradual Typing.
Research Seminar. University of Chile. January, 2016.
[slides.pdf] [slides.key] [demo.agda] -
Formally Verifying and Deriving Gradual Type Systems.
Class Presentation. University of Maryland CMSC 631. December, 2015.
[slides.pdf] [slides.key] -
Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis.
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA). Pittsburgh, Pennsylvania, USA. October, 2015.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video]
Professional Activities
-
Upcoming
- OOPSLA 2019: Student Research Competition Co-chair
- Past
- ICFP 2018: External Review Committee (ERC)
- TyDe 2018: Program Committee (PC)
- IFL 2018: Program Committee (PC)
- SPLASH 2017: Video Co-Chair
- PLDI 2017: Video Chair
- ECOOP 2017: Doctoral Symposium Co-chair, Video Chair
- POPL 2017: Video Co-Chair
- ECOOP 2016: Video Chair
- PLDI 2016: Video Co-Chair
- POPL 2016: Artifact Evaluation Committee (AEC), Student Volunteer
- ICFP 2013: Student Volunteer Chair, Video Chair, Logo Designer
Short Bio
David Darais is an assistant professor at the University of Vermont. David's research focuses on tools for achieving highly reliable software for critical and security-sensitive systems. David received a BS in Computer Science from University of Utah, an MS in Computer Science from Harvard University, and a PhD in Computer Science from University of Maryland.Links
- On Preparing Talks (by Ranjit Jhala at UCSD, ICFP PLMW 2018)