David Darais
@daviddarais Twitter Logo
@davdar Github Logo

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

I'm a PhD student in computer science supervised by David Van Horn. I study program analysis metatheory, mechanized proofs, and certified functional programming. I'm a member of the PLUM group at University of Maryland, College Park.

Constructive Galois Connections

Most recently I developed Constructive Galois Connections (with Van Horn, Preprint March 2016), which solves the open problem of embedding Galois connections in a proof assistant. Our insight is to identify a restricted subset of Galois connections which can be mechanized effectively, and which also support the benefits of a general abstraction framework.

Constructive Galois connections enable a mode of use which the state of the art in verification is unable to capture: calculating the definition of an abstract interpreter from its specification. Calculations in our framework explicitly discharge a "specification effect", moving from specification to algorithm within a unified theory, and do so without the use of classical axioms, which is essential for verified program extraction. Our framework enables the design of mechanically verified static analyzers which are both sound and computable by construction.

Abstracting Definitional Interpreters

Also recently I developed Abstracting Definitional Interpreters (with Labich, Nguyễn and Van Horn, Preprint March 2016), a framework for designing static analyzers from big-step interpreters. Using the framework, we easily recover a wide range of static analyzers, including a symbolic executor and pushdown analyzer. In particular, the pushdown property is inherited from the precise call-return matching of the metalanguage, à la Reynolds. We achieve these results by combining big-step interpreters, monad transformers, and a novel fixpoint iteration strategy for the big-step setting.

Galois Transformers

I developed Galois Transformers (with Might and Van Horn, OOPSLA 2015), a compositional framework for building static analyzers. Our framework synthesizes large families of analyses and their proofs of soundness for free. We also show how to compose choices in flow sensitivity with other analysis features within the framework. We achieve these results by combining abstract interpretation, monad transformers and small-step monadic interpreters.




Last updated March 24, 2016