A Type and Effect System for Flexible Abstract Interpretation of Java: (Extended Abstract). - Christian Skalka; Scott F. Smith 001; David Van Horn (AIOOL@VMCAI, 2005)

Relating complexity and precision in control flow analysis. - David Van Horn; Harry G. Mairson (ICFP, 2007)

Deciding kCFA is complete for EXPTIME. - David Van Horn; Harry G. Mairson (ICFP, 2008)

Flow Analysis, Linearity, and PTIME. - David Van Horn; Harry G. Mairson (SAS, 2008)

Types and trace effects of higher order programs. - Christian Skalka; Scott F. Smith 001; David Van Horn (J. Funct. Program., 2008)

Abstracting abstract machines. - David Van Horn; Matthew Might (ICFP, 2010)

Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. - Matthew Might; Yannis Smaragdakis; David Van Horn (PLDI, 2010)

Evaluating Call-by-Need on the Control Stack. - Stephen Chang 001; David Van Horn; Matthias Felleisen (Trends in Functional Programming, 2010)

Pushdown Control-Flow Analysis of Higher-Order Programs - Christopher Earl; Matthew Might; David Van Horn (CoRR, 2010)

Stack-Summarizing Control-Flow Analysis of Higher-Order Programs - Christopher Earl; Matthew Might; David Van Horn (CoRR, 2010)

A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs. - Matthew Might; David Van Horn (SAS, 2011)

Abstracting abstract machines: a systematic approach to higher-order program analysis. - David Van Horn; Matthew Might (Commun. ACM, 2011)

Modular Analysis via Specifications as Values - Sam Tobin-Hochstadt; David Van Horn (CoRR, 2011)

Semantic Solutions to Program Analysis Problems - Sam Tobin-Hochstadt; David Van Horn (CoRR, 2011)

An Analytic Framework for JavaScript - David Van Horn; Matthew Might (CoRR, 2011)

Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5). - Naoki Kobayashi 001; Luke Ong; David Van Horn (NII Shonan Meet. Rep., 2011)

Introspective pushdown analysis of higher-order programs. - Christopher Earl; Ilya Sergey; Matthew Might; David Van Horn (ICFP, 2012)

Higher-order symbolic execution via contracts. - Sam Tobin-Hochstadt; David Van Horn (OOPSLA, 2012)

Optimizing Abstract Abstract Machines - Dionna Amalie Glaze; Matthew Might; David Van Horn (CoRR, 2012)

Systematic abstraction of abstract machines. - David Van Horn; Matthew Might (J. Funct. Program., 2012)

Realm of Racket - Learn to Program, One Game at a Time! - Matthias Felleisen; David Van Horn; Conrad Barski (No Starch Press, 2013)

Sound and precise malware analysis for android via pushdown reachability and entry-point saturation. - Shuying Liang; Andrew W. Keep; Matthew Might; Steven Lyde; Thomas Gilray; Petey Aldous; David Van Horn (SPSM@CCS, 2013)

Optimizing abstract abstract machines. - Dionna Amalie Glaze; Nicholas Labich; Matthew Might; David Van Horn (ICFP, 2013)

The Complexity of Flow Analysis in Higher-Order Languages. - David Van Horn (CoRR, 2013)

Deciding $k$CFA is complete for EXPTIME. - David Van Horn; Harry G. Mairson (CoRR, 2013)

Resolving and Exploiting the $k$-CFA Paradox. - Matthew Might; Yannis Smaragdakis; David Van Horn (CoRR, 2013)

Static Contract Checking for Scripting Languages. - Phuc C. Nguyen; Sam Tobin-Hochstadt; David Van Horn (CoRR, 2013)

From Principles to Practice with Class in the First Year. - Sam Tobin-Hochstadt; David Van Horn (TFPIE, 2013)

Pushdown Exception-Flow Analysis of Object-Oriented Programs - Shuying Liang; Matthew Might; Thomas Gilray; David Van Horn (CoRR, 2013)

Concrete Semantics for Pushdown Analysis: The Essence of Summarization - Dionna Amalie Glaze; David Van Horn (CoRR, 2013)

AnaDroid: Malware Analysis of Android with User-supplied Predicates. - Shuying Liang; Matthew Might; David Van Horn (TAPAS@SAS, 2013)

Abstracting abstract control. - Dionna Amalie Glaze; David Van Horn (DLS, 2014)

Soft contract verification. - Phuc C. Nguyen; Sam Tobin-Hochstadt; David Van Horn (ICFP, 2014)

Pruning, Pushdown Exception-Flow Analysis. - Shuying Liang; Weibin Sun; Matthew Might; Andrew W. Keep; David Van Horn (SCAM, 2014)

Galois Transformers and Modular Abstract Interpreters. - David Darais; Matthew Might; David Van Horn (CoRR, 2014)

Pushdown flow analysis with abstract garbage collection. - Dionna Amalie Glaze; Ilya Sergey; Christopher Earl; Matthew Might; David Van Horn (J. Funct. Program., 2014)

Running Probabilistic Programs Backwards. - Neil Toronto; Jay McCarthy; David Van Horn (ESOP, 2015)

Galois transformers and modular abstract interpreters: reusable metatheory for program analysis. - David Darais; Matthew Might; David Van Horn (OOPSLA, 2015)

Incremental computation with names. - Matthew A. Hammer; Jana Dunfield; Kyle Headley; Nicholas Labich; Jeffrey S. Foster; Michael W. Hicks; David Van Horn (OOPSLA, 2015)

Relatively complete counterexamples for higher-order programs. - Phuc C. Nguyen; David Van Horn (PLDI, 2015)

The use of analytics in the design of sociotechnical products. - David Van Horn; Kemper Lewis (Artif. Intell. Eng. Des. Anal. Manuf., 2015)

Mechanically Verified Calculational Abstract Interpretation. - David Darais; David Van Horn (CoRR, 2015)

A vision for online verification-validation. - Matthew A. Hammer; Bor-Yuh Evan Chang; David Van Horn (GPCE, 2016)

Constructive Galois connections: taming the Galois connection framework for mechanized metatheory. - David Darais; David Van Horn (ICFP, 2016)

Pushdown control-flow analysis for free. - Thomas Gilray; Steven Lyde; Michael D. Adams 001; Matthew Might; David Van Horn (POPL, 2016)

Abstracting Definitional Interpreters. - David Darais; Nicholas Labich; Phuc C. Nguyen; David Van Horn (CoRR, 2017)

Higher order symbolic execution for contract verification and refutation. - Phuc C. Nguyen; Sam Tobin-Hochstadt; David Van Horn (J. Funct. Program., 2017)

Abstracting definitional interpreters (functional pearl). - David Darais; Nicholas Labich; Phuc C. Nguyen; David Van Horn (Proc. ACM Program. Lang., 2017)

Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). - Niki Vazou; Joachim Breitner; Rose Kunkel; David Van Horn; Graham Hutton (Haskell@ICFP, 2018)

Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell). - Niki Vazou; Joachim Breitner; Will Kunkel; David Van Horn; Graham Hutton (CoRR, 2018)

Size-Change Termination as a Contract. - Phuc C. Nguyen; Thomas Gilray; Sam Tobin-Hochstadt; David Van Horn (CoRR, 2018)

Soft contract verification for higher-order stateful programs. - Phuc C. Nguyen; Thomas Gilray; Sam Tobin-Hochstadt; David Van Horn (Proc. ACM Program. Lang., 2018)

Gradual liquid type inference. - Niki Vazou; Éric Tanter; David Van Horn (Proc. ACM Program. Lang., 2018)

Type-level computations for Ruby libraries. - Milod Kazerounian; Sankha Narayan Guria; Niki Vazou; Jeffrey S. Foster; David Van Horn (PLDI, 2019)

Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs. - Phuc C. Nguyen; Thomas Gilray; Sam Tobin-Hochstadt; David Van Horn (PLDI, 2019)

Constructive Galois Connections. - David Darais; David Van Horn (J. Funct. Program., 2019)

RbSyn: type- and effect-guided program synthesis. - Sankha Narayan Guria; Jeffrey S. Foster; David Van Horn (PLDI, 2021)

Corpse reviver: sound and efficient gradual typing via contract verification. - Cameron Moy; Phuc C. Nguyen; Sam Tobin-Hochstadt; David Van Horn (Proc. ACM Program. Lang., 2021)

A formal model of Checked C. - Liyi Li 002; Yiyun Liu; Deena L. Postol; Leonidas Lampropoulos; David Van Horn; Michael Hicks 001 (J. Comput. Secur., 2023)

Absynthe: Abstract Interpretation-Guided Synthesis. - Sankha Narayan Guria; Jeffrey S. Foster; David Van Horn (Proc. ACM Program. Lang., 2023)

Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis. - Benjamin Quiring; David Van Horn (Proc. ACM Program. Lang., 2024)

Webs and Flow-Directed Well-Typedness Preserving Program Transformations. - Benjamin Quiring; David Van Horn; John H. Reppy; Olin Shivers (Proc. ACM Program. Lang., 2025)