David Van Horn

Publication Activity (10 Years)

Years Active: 2005-2023
Publications (10 Years): 39

Top Topics

Abstract Interpretation

Garbage Collection

Galois Lattices

Top Venues

Proc. ACM Program. Lang.

Publications

Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
Absynthe: Abstract Interpretation-Guided Synthesis. CoRR (2023)
Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
Absynthe: Abstract Interpretation-Guided Synthesis. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
A formal model of Checked C. J. Comput. Secur. 31 (5) (2023)
Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
A Formal Model of Checked C. CoRR (2022)
Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
A Formal Model of Checked C. CSF (2022)
Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
RbSyn: Type- and Effect-Guided Program Synthesis. CoRR (2021)
Cameron Moy, Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
Corpse reviver: sound and efficient gradual typing via contract verification. Proc. ACM Program. Lang. 5 (POPL) (2021)
Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
RbSyn: type- and effect-guided program synthesis. PLDI (2021)
Cameron Moy, Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification. CoRR (2020)
Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs. PLDI (2019)
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn
Type-Level Computations for Ruby Libraries. CoRR (2019)
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn
Type-level computations for Ruby libraries. PLDI (2019)
David Darais, David Van Horn
Constructive Galois Connections. J. Funct. Program. 29 (2019)
David Darais, David Van Horn
Constructive Galois Connections. CoRR (2018)
Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, Graham Hutton
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). Haskell@ICFP (2018)
Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, Graham Hutton
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell). CoRR (2018)
Niki Vazou, Éric Tanter, David Van Horn
Gradual liquid type inference. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
Size-Change Termination as a Contract. CoRR (2018)
Niki Vazou, Éric Tanter, David Van Horn
Gradual Liquid Type Inference. CoRR (2018)
Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
Soft contract verification for higher-order stateful programs. Proc. ACM Program. Lang. 2 (POPL) (2018)
David Darais, Nicholas Labich, Phuc C. Nguyen, David Van Horn
Abstracting Definitional Interpreters. CoRR (2017)
David Darais, Nicholas Labich, Phuc C. Nguyen, David Van Horn
Abstracting definitional interpreters (functional pearl). Proc. ACM Program. Lang. 1 (ICFP) (2017)
Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
Soft Contract Verification for Higher-Order Stateful Programs. CoRR (2017)
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
Higher order symbolic execution for contract verification and refutation. J. Funct. Program. 27 (2017)
Matthew A. Hammer, Bor-Yuh Evan Chang, David Van Horn
A vision for online verification-validation. GPCE (2016)
David Darais, David Van Horn
Constructive Galois connections: taming the Galois connection framework for mechanized metatheory. ICFP (2016)
Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn
Pushdown control-flow analysis for free. POPL (2016)
Matthew A. Hammer, Bor-Yuh Evan Chang, David Van Horn
A Vision for Online Verification-Validation. CoRR (2016)
Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks, David Van Horn
Incremental computation with names. OOPSLA (2015)
David Darais, Matthew Might, David Van Horn
Galois transformers and modular abstract interpreters: reusable metatheory for program analysis. OOPSLA (2015)
Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael Hicks, David Van Horn
Incremental Computation with Names. CoRR (2015)
David Darais, David Van Horn
Mechanically Verified Calculational Abstract Interpretation. CoRR (2015)
David Darais, David Van Horn
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory. CoRR (2015)
David Van Horn, Kemper Lewis
The use of analytics in the design of sociotechnical products. Artif. Intell. Eng. Des. Anal. Manuf. 29 (1) (2015)
Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn
Pushdown Control-Flow Analysis for Free. CoRR (2015)
Phuc C. Nguyen, David Van Horn
Relatively complete counterexamples for higher-order programs. PLDI (2015)
Shuying Liang, Matthew Might, David Van Horn
AnaDroid: Malware Analysis of Android with User-supplied Predicates. Electron. Notes Theor. Comput. Sci. 311 (2015)
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
Higher-order symbolic execution for contract verification and refutation. CoRR (2015)
Neil Toronto, Jay McCarthy, David Van Horn
Running Probabilistic Programs Backwards. ESOP (2015)
J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn
Pushdown flow analysis with abstract garbage collection. J. Funct. Program. 24 (2-3) (2014)
Neil Toronto, Jay McCarthy, David Van Horn
Running Probabilistic Programs Backwards. CoRR (2014)
David Darais, Matthew Might, David Van Horn
Galois Transformers and Modular Abstract Interpreters. CoRR (2014)
Phuc C. Nguyen, David Van Horn
Relatively Complete Counterexamples for Higher-Order Programs. CoRR (2014)
Shuying Liang, Weibin Sun, Matthew Might, Andrew W. Keep, David Van Horn
Pruning, Pushdown Exception-Flow Analysis. SCAM (2014)
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
Soft contract verification. ICFP (2014)
Shuying Liang, Weibin Sun, Matthew Might, Andrew W. Keep, David Van Horn
Pruning, Pushdown Exception-Flow Analysis. CoRR (2014)
James Ian Johnson, David Van Horn
Abstracting abstract control. DLS (2014)
J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn
Pushdown flow analysis with abstract garbage collection. CoRR (2014)
Matthew Might, Yannis Smaragdakis, David Van Horn
Resolving and Exploiting the $k$-CFA Paradox. CoRR (2013)
Shuying Liang, Matthew Might, David Van Horn
AnaDroid: Malware Analysis of Android with User-supplied Predicates. CoRR (2013)
David Van Horn
The Complexity of Flow Analysis in Higher-Order Languages. CoRR (2013)
David Van Horn, Harry G. Mairson
Deciding $k$CFA is complete for EXPTIME. CoRR (2013)
David Van Horn, Harry G. Mairson
Flow analysis, linearity, and PTIME. CoRR (2013)
Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, Petey Aldous, David Van Horn
Sound and precise malware analysis for android via pushdown reachability and entry-point saturation. SPSM@CCS (2013)
J. Ian Johnson, Nicholas Labich, Matthew Might, David Van Horn
Optimizing abstract abstract machines. ICFP (2013)
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
Static Contract Checking for Scripting Languages. CoRR (2013)
J. Ian Johnson, David Van Horn
Concrete Semantics for Pushdown Analysis: The Essence of Summarization CoRR (2013)
Shuying Liang, Matthew Might, Thomas Gilray, David Van Horn
Pushdown Exception-Flow Analysis of Object-Oriented Programs CoRR (2013)
Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, Petey Aldous, David Van Horn
Sound and Precise Malware Analysis for Android via Pushdown Reachability and Entry-Point Saturation. CoRR (2013)
Sam Tobin-Hochstadt, David Van Horn
From Principles to Practice with Class in the First Year. TFPIE (2013)
David Van Horn, Matthew Might
Systematic abstraction of abstract machines. J. Funct. Program. 22 (4-5) (2012)
Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn
Introspective Pushdown Analysis of Higher-Order Programs CoRR (2012)
Sam Tobin-Hochstadt, David Van Horn
Higher-order symbolic execution via contracts. OOPSLA (2012)
Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn
Introspective pushdown analysis of higher-order programs. ICFP (2012)
J. Ian Johnson, Matthew Might, David Van Horn
Optimizing Abstract Abstract Machines CoRR (2012)
David Van Horn, Matthew Might
Systematic Abstraction of Abstract Machines CoRR (2011)
Naoki Kobayashi, Luke Ong, David Van Horn
Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5). NII Shonan Meet. Rep. 2011 (2011)
David Van Horn, Matthew Might
Abstracting Abstract Machines: A Systematic Approach to Higher-Order Program Analysis CoRR (2011)
Sam Tobin-Hochstadt, David Van Horn
Modular Analysis via Specifications as Values CoRR (2011)
Sam Tobin-Hochstadt, David Van Horn
Semantic Solutions to Program Analysis Problems CoRR (2011)
Matthew Might, David Van Horn
A family of abstract interpretations for static analysis of concurrent higher-order programs CoRR (2011)
Matthew Might, David Van Horn
A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs. SAS (2011)
David Van Horn, Matthew Might
An Analytic Framework for JavaScript CoRR (2011)
David Van Horn, Matthew Might
Abstracting abstract machines: a systematic approach to higher-order program analysis. Commun. ACM 54 (9) (2011)
Christopher Earl, Matthew Might, David Van Horn
Pushdown Control-Flow Analysis of Higher-Order Programs CoRR (2010)
Stephen Chang, David Van Horn, Matthias Felleisen
Evaluating Call-by-Need on the Control Stack. Trends in Functional Programming (2010)
David Van Horn, Matthew Might
Abstracting abstract machines. ICFP (2010)
Matthew Might, Yannis Smaragdakis, David Van Horn
-CFA paradox: illuminating functional vs. object-oriented program analysis. PLDI (2010)
Christopher Earl, Matthew Might, David Van Horn
Stack-Summarizing Control-Flow Analysis of Higher-Order Programs CoRR (2010)
David Van Horn, Matthew Might
Abstracting Abstract Machines CoRR (2010)
Stephen Chang, David Van Horn, Matthias Felleisen
Evaluating Call-By-Need on the Control Stack CoRR (2010)
Christian Skalka, Scott F. Smith, David Van Horn
Types and trace effects of higher order programs. J. Funct. Program. 18 (2) (2008)
David Van Horn, Harry G. Mairson
Flow Analysis, Linearity, and PTIME. SAS (2008)
David Van Horn, Harry G. Mairson
CFA is complete for EXPTIME. ICFP (2008)
David Van Horn, Harry G. Mairson
Relating complexity and precision in control flow analysis. ICFP (2007)
Christian Skalka, Scott F. Smith, David Van Horn
A Type and Effect System for Flexible Abstract Interpretation of Java: (Extended Abstract). Electron. Notes Theor. Comput. Sci. 131 (2005)