David Darais
darais@cs.umd.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.

My research is aimed at achieving highly reliable software. Current methods for software reliability are either insufficient for critical software (don't catch all bugs), or too expensive to implement (require too much effort). 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 can be reused to automate the verification of software reliability, reducing the manual effort required. I then mechanically verify these program analyzers so their results can be trusted to achieve high assurance in software reliability. Finally, I design reusable fragments of analyzers which can be composed by non-experts to build mechanically verified analyzers for new programming languages and analysis domains.

Constructive Galois Connections

Recently 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.

Definitional Abstract Interpreters

Also recently 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.

Publications

Theses

Workshops

Drafts

Talks

Professional Activities

Teaching

Last updated August 22, 2017