David Darais
Assistant Professor
Computer Science
University of Vermont
Votey 319

David.Darais@uvm.edu
@daviddarais Twitter Logo
@davdar Github Logo

★ 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

Publications

Theses

Workshops

Drafts

Talks

Professional Activities

Short Bio

David Darais is an Assistant Professor at the University of Vermont. David's research focuses on tools for achieving reliable software in critical, security-sensitive, and privacy-sensitive systems. David received his BS, MS and PhD from University of Utah, Harvard University and University of Maryland.

Links

My CV