David Darais

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.

Most recently I developed Mechanically Verified Calculational Abstract Interpretation (with Van Horn, 2015), which solves the open problem of embedding calculational approaches to abstract interpretation in proof assistants. The root of the problem is the inability to encode classical Galois connections in a constructive framework. Our solution is to redevelop Galois connections in a constructive setting using a modality with monadic structure. Calculation then explicitly discharges the classical "specification effect" resulting in a mechanically verified and executable abstract interpreter.

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 Aug 26, 2015