Travelled to:1 × Denmark
1 × Germany
1 × Italy
1 × Spain
1 × Sweden
1 × The Netherlands
1 × United Kingdom
3 × Canada
6 × USA
Collaborated with:M.Might S.Tobin-Hochstadt H.G.Mairson P.C.Nguyen N.Vazou Thomas Gilray M.A.Hammer N.Labich J.S.Foster N.Toronto J.McCarthy D.Darais Y.Smaragdakis B.E.Chang É.Tanter J.I.Johnson C.Earl I.Sergey S.Liang W.Sun A.W.Keep J.Breitner R.Kunkel G.Hutton Steven Lyde M.D.A.0001 Milod Kazerounian S.N.Guria J.Dunfield K.Headley M.W.Hicks
Talks about:program (8) analysi (8) abstract (6) higher (6) order (6) contract (4) flow (4) pushdown (3) verif (3) interpret (2)
Person: David Van Horn
DBLP: Horn:David_Van
Contributed to:
2015
2015
2015
2014
20142013
201320122012
201120102010200820082007
2016
20182018
201620182019Wrote 23 papers:
- ESOP-2015-TorontoMH #probability #source code
- Running Probabilistic Programs Backwards (NT, JM, DVH), pp. 53–79.
- OOPSLA-2015-DaraisMH #composition #program analysis #reuse
- Galois transformers and modular abstract interpreters: reusable metatheory for program analysis (DD, MM, DVH), pp. 552–571.
- OOPSLA-2015-HammerDHLFHH #incremental
- Incremental computation with names (MAH, JD, KH, NL, JSF, MWH, DVH), pp. 748–766.
- PLDI-2015-NguyenH #higher-order #source code
- Relatively complete counterexamples for higher-order programs (PCN, DVH), pp. 446–456.
- ICFP-2014-NguyenTH #contract #verification
- Soft contract verification (PCN, STH, DVH), pp. 139–152.
- SCAM-2014-LiangSMKH #analysis #automaton #exception
- Pruning, Pushdown Exception-Flow Analysis (SL, WS, MM, AWK, DVH), pp. 265–274.
- ICFP-2013-JohnsonLMH #automaton #optimisation
- Optimizing abstract abstract machines (JIJ, NL, MM, DVH), pp. 443–454.
- TFPIE-2013-Tobin-HochstadtH
- From Principles to Practice with Class in the First Year (STH, DVH), pp. 1–15.
- ICFP-2012-EarlSMH #analysis #automaton #higher-order #source code
- Introspective pushdown analysis of higher-order programs (CE, IS, MM, DVH), pp. 177–188.
- OOPSLA-2012-Tobin-HochstadtH #contract #execution #higher-order #symbolic computation
- Higher-order symbolic execution via contracts (STH, DVH), pp. 537–554.
- SAS-2011-MightH #abstract interpretation #concurrent #higher-order #product line #source code #static analysis
- A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs (MM, DVH), pp. 180–197.
- ICFP-2010-HornM #automaton
- Abstracting abstract machines (DVH, MM), pp. 51–62.
- PLDI-2010-MightSH #functional #object-oriented #program analysis
- Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis (MM, YS, DVH), pp. 305–315.
- ICFP-2008-HornM
- Deciding kCFA is complete for EXPTIME (DVH, HGM), pp. 275–282.
- SAS-2008-HornM #analysis
- Flow Analysis, Linearity, and PTIME (DVH, HGM), pp. 255–269.
- ICFP-2007-HornM #analysis #complexity #control flow #precise
- Relating complexity and precision in control flow analysis (DVH, HGM), pp. 85–96.
- GPCE-2016-HammerCH #online
- A vision for online verification-validation (MAH, BYEC, DVH), pp. 190–201.
- Haskell-2018-VazouBKHH #equation #functional #haskell #proving #reasoning #theorem proving
- Theorem proving for all: equational reasoning in liquid Haskell (functional pearl) (NV, JB, RK, DVH, GH), pp. 132–144.
- OOPSLA-2018-VazouTH #type inference
- Gradual liquid type inference (NV, ÉT, DVH), p. 25.
- POPL-2016-GilrayL0MH #analysis #automaton #control flow #for free
- Pushdown control-flow analysis for free (TG, SL, MDA0, MM, DVH), pp. 691–704.
- POPL-2018-NguyenGTH #contract #higher-order #source code #verification
- Soft contract verification for higher-order stateful programs (PCN, TG, STH, DVH), p. 30.
- PLDI-2019-KazerounianGVFH #library #ruby
- Type-level computations for Ruby libraries (MK, SNG, NV, JSF, DVH), pp. 966–979.
- PLDI-2019-NguyenGTH #contract #higher-order #source code #termination
- Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs (PCN, TG, STH, DVH), pp. 845–859.