David Darais
University of Maryland
Post-doctoral Researcher
darais@cs.umd.edu
David.Darais@uvm.edu
@daviddarais Twitter Logo
@davdar Github Logo

University of Maryland
A.V. Williams Rm. 3452
8223 Paint Branch Dr.
College Park, MD 20742

★ I will join the University of Vermont as tenure-track Assistant Professor in Computer Science starting January 2018. I am looking for PhD students to work with me starting then (or possibly sooner) in programming languages and/or computer security.

I am currently a Post-doctoral researcher in computer science supervised by David Van Horn at the University of Maryland PLUM lab. 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 reliability of software. I then mechanically verify these program analyzers so their results can be trusted to achieve high assurance for 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.

Publications

Theses

Workshops

Drafts

Talks

Professional Activities

Teaching

Short Bio

David Darais is a post-doctoral researcher at the University of Maryland and will join the faculty at the University of Vermont in January 2018. 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.

CV

Last updated November 29, 2017