David Darais
@daviddarais Twitter Logo

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

I'm currently a PhD student in computer science under the supervision of David Van Horn. I study program analysis metatheory and formally verified 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 and Mechanically Verified Calculational Abstract Interpretation (w/Van Horn, Preprints November and July 2015), which solves the open problem of embedding Galois connections in a proof assistant. Our insight is to redevelop the theory of Galois connections in a constructive setting using a monad which explicitly separates classical specifications from constructive algorithms.

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 abstract interpreters which are sound and computable by construction.

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 monadic interpreters.



Last updated Nov 24, 2015