David Van Horn

Associate Professor
Department of Computer Science
& UMIACS
University of Maryland

UMD

Structures don’t march in the streets.


Projects

Gradual Verification: From Scripting to Proving (PI)

Online Verification-Validation (PI)

The Science and Applications of Crypto-Currency (Co-PI)

Sound Over- and Under-Approximation of Complexity and Information Security (Co-PI)

Trustworthy and Composable Software Systems with Contracts (PI)

Behavioral Software Contract Verification (Co-PI)

Scalable and precise abstractions of programs for trustworthy software (PI)

Raising the level of discourse with GnoSys (Senior personnel)


Students

Current
Past

Papers

A Formal Model of Checked C. With Liyi Li, Yiyun Liu, Deena Postol, Leonidas Lampropoulos, and Michael Hicks.
IEEE Computer Security Foundations Symposium, Haifa, Israel, August 2022.
arXiv ]

RbSyn: Type- and Effect-Guided Program Synthesis. With Sankha Guria and Jeffrey S. Foster.
The ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21), Online, June 2021.
ACM | arXiv ]

Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification. With Cameron Moy, Phúc C. Nguyễn, and Sam Tobin-Hochstadt.
The 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'21), Online, January 2021.
ACM | arXiv ]

Constructive Galois Connections. With David Darais.
Journal of Functional Programming, 29(11), July 2019.
CUP | arXiv ]

Size-Change Termination as a Contract. With Phúc C. Nguyễn, Thomas Gilray, and Sam Tobin-Hochstadt.
The ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'19), Phoenix, Arizona, June 2019.
ACM | arXiv ]

Type-Level Computations for Ruby Libraries. With Milod Kazerounian, Sankha Guria, Niki Vazou, and Jeffrey S. Foster.
The ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'19), Phoenix, Arizona, June 2019.
ACM | arXiv ]

Gradual Liquid Type Inference (Distinguished Paper). With Niki Vazou and Éric Tanter.
The ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'18), Boston, USA, October 2018.
ACM | arXiv ]

Theorem Proving for All: Equational Reasoning in Liquid Haskell. With Niki Vazou, Joachim Breitner, Rose Kunkel, and Graham Hutton.
The ACM SIGPLAN International Symposium on Haskell (Haskell'18), St. Louis, Missouri, September 2018.
ACM | arXiv ]

Soft Contract Verification for Higher-order Stateful Programs. With Phúc C. Nguyễn, Thomas Gilray, and Sam Tobin-Hochstadt.
The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'18), Los Angeles, USA, January 2018.
ACM | arXiv ]

Abstracting Definitional Interpreters. With David Darais, Phúc C. Nguyễn, and Nicholas Labich.
The ACM SIGPLAN International Conference on Functional Programming (ICFP'17), Oxford, UK, September 2017.
ACM | arXiv ]

Higher-order symbolic execution for contract verification and refutation. With Phúc C. Nguyễn and Sam Tobin-Hochstadt.
Journal of Functional Programming, 27(3), January 2017.
CUP | arXiv ]

A Vision for Online Verification-Validation. With Matthew A. Hammer and Bor-Yuh Evan Chang.
The 15th International Conference on Generative Programming: Concepts & Experience (GPCE'16), Amsterdam, Netherlands, November 2016.
ACM | arxiv ]

Constructive Galois Connections. With David Darais.
The ACM SIGPLAN International Conference on Functional Programming (ICFP'16), Nara, Japan, September 2016.
ACM | arXiv ]

Pushdown Control-Flow Analysis for Free. With Thomas Gilray, Steven Lyde, Michael D. Adams, and Matthew Might.
The 43rd ACM SIGPLAN-SIGACT Symposium on Principles in Programming Languages (POPL'16), St. Petersburg, Florida, January 2016.
ACM | arXiv ]

Tutorial: An Introduction to Redex with Abstracting Abstract Machines.
Tutorials at The 43rd ACM SIGPLAN-SIGACT Symposium on Principles in Programming Languages (POPL'16), St. Petersburg, Florida, January 2016.
HTML | PDF ]

Incremental Computation with Names. With Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, and Michael Hicks.
The ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'15), Pittsburgh, Pennsylvania, October 2015.
ACM | arXiv ]

Galois Transformers and Modular Abstract Interpreters. With David Darais and Matthew Might.
The ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'15), Pittsburgh, Pennsylvania, October 2015.
ACM | arXiv ]

Relatively Complete Counterexamples for Higher-Order Programs. With Phúc C. Nguyễn.
The 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), Portland, Oregon, June, 2015.
ACM | arXiv ]

Running Probabilistic Programs Backwards. With Neil Toronto and Jay McCarthy.
The European Symposium on Programming (ESOP'15), London, United Kingdom, April, 2015.
Springer | arXiv ]

Abstracting Abstract Control. With Dionna Amalie Glaze.
The 10th ACM Symposium on Dynamic Languages (DLS'14), Portland, Oregon, October 2014.
ACM | arXiv ]

Pruning, Pushdown Exception-Flow Analysis. With Shuying Liang, Weibin Sun, Matthew Might, and Andrew W. Keep.
The 14th IEEE International Conference on Software Code Analysis and Manipulation, Victoria, British Columbia, September 2014.
IEEE | arXiv ]

Soft Contract Verification. With Phúc C. Nguyễn and Sam Tobin-Hochstadt.
The ACM SIGPLAN International Conference on Functional Programming (ICFP'14), Gothenburg, Sweden, September 2014.
ACM | arXiv ]

Pushdown flow analysis with abstract garbage collection. With Dionna Amalie Glaze, Ilya Sergey, Christopher Earl, and Matthew Might.
Journal of Functional Programming, 24(2-3), May 2014.
CUP | arXiv ]

Optimizing Abstract Abstract Machines. With Dionna Amalie Glaze, Nicholas Labich, and Matthew Might.
The ACM SIGPLAN International Conference on Functional Programming (ICFP'13), Boston, Massachusetts, September 2013.
ACM | arXiv ]

Sound and Precise Malware Analysis for Android via Pushdown Reachability and Entry-Point Saturation. With Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, and Petey Aldous.
Proceedings of the Third ACM workshop on Security and privacy in smartphones & mobile devices, Berlin, Germany, November 2013.
ACM | arXiv ]

AnaDroid: Malware Analysis of Android with User-supplied Predicates. With Shuying Liang and Matthew Might.
Workshop on Tools for Automatic Program Analysis, Seattle, Washington, June 2013.
arXiv ]

Concrete Semantics for Pushdown Analysis: The Essence of Summarization. With Dionna Amalie Glaze.
Workshop on Higher-Order Program Analysis, New Orleans, Louisiana, June 2013.
arXiv ]

From Principles to Practice with Class in the First Year. With Sam Tobin-Hochstadt.
International Workshop on Trends in Functional Programming in Education, Provo, Utah, May 2013.
EPCTCS | arXiv ]

Higher-Order Symbolic Execution via Contracts. With Sam Tobin-Hochstadt.
The ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12), Tuscon, Arizona, October 2012.
ACM | arXiv ]

Introspective Pushdown Analysis of Higher-Order Programs. With Christopher Earl, Ilya Sergey, and Matthew Might.
The 17th ACM SIGPLAN International Conference on Functional Programming (ICFP'12), Copenhagen, Denmark, September 2012.
ACM | arXiv ]

Systematic Abstraction of Abstract Machines. With Matthew Might.
Journal of Functional Programming, 22(4-5), September 2012.
CUP | arXiv ]

Abstracting Abstract Machines. With Matthew Might.
Communications of the ACM, Research Highlights, 54(9), September 2011.
ACM | arXiv ]

A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs. With Matthew Might.
The 18th International Static Analysis Symposium (SAS 2011), Venice, Italy, September 2011.
Springer | arXiv ]

Semantic Solutions to Program Analysis Problems. With Sam Tobin-Hochstadt.
FIT Session, The ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation (PLDI'11), San Jose, California, June 2011.
arXiv ]

Abstracting Abstract Machines. With Matthew Might.
The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP'10), Baltimore, Maryland, September 2010.
ACM | arXiv ]

Pushdown Control-Flow Analysis of Higher-Order Programs. With Christopher Earl and Matthew Might.
The 2010 Workshop on Scheme and Functional Programming (SFP'10), Montréal, Québec, August 2010.
arXiv ]

Evaluating Call-By-Need on the Control Stack. With Stephen Chang and Matthias Felleisen.
Symposium on Trends in Functional Programming (TFP 2010), Norman, Oklahoma, May 2010.
Springer | arXiv ]

Resolving and Exploiting the k-CFA Paradox. With Matthew Might and Yannis Smaragdakis.
The ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI'10), Toronto, Canada, June 2010.
ACM | arXiv ]

The Complexity of Flow Analysis in Higher-Order Languages.
PhD dissertation, Brandeis University, August 2009.
UMI | arXiv ]

Deciding kCFA is complete for EXPTIME. With Harry G. Mairson.
The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08), Victoria, British Columbia, Canada, September 2008.
ACM | arXiv ]

Flow Analysis, Linearity, and PTIME. With Harry G. Mairson.
The 15th International Static Analysis Symposium (SAS 2008), Valencia, Spain, July 2008.
Springer | arXiv ]

Types and Trace Effects of Higher Order Programs. With Christian Skalka and Scott F. Smith.
Journal of Functional Programming, 18(2), March 2008.
CUP ]

Relating Complexity and Precision in Control Flow Analysis. With Harry G. Mairson.
The Twelth ACM SIGPLAN International Conference on Functional Programming (ICFP'07), Freiburg, Germany, October 2007.
ACM ]

Algorithmic Trace Effect Analysis.
MS thesis, University of Vermont, May 2006.
UVM ]

A Type and Effect System for Flexible Abstract Interpretation of Java. With Christian Skalka and Scott F. Smith.
The ACM Workshop on Abstract Interpretations of Object-Oriented Programs, Paris, France, January 2005.
Elsevier ]


Talks

Symbolic Execution for Higher-Order Program Verification
University of Washington, UCLA Compilers Colloquium, Los Angeles, California, April 2018
Symbolic Execution for Higher-Order Program Verification
University of Washington, PLSE Colloquium, Seattle, Washington, April 2018
Redex, Abstract Machines, and Abstract Interpretation
Oregon Programming Languages Summer School (OPLSS), University of Oregon, Eugene, Oregon, July 2017
Tutorial: Introduction to Redex with Abstracting Abstract Machines
Tutorials at the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida, January 2016
Verification and Refutation of Behavioral Contracts with Higher-Order Symbolic Execution
University of Chile, PLEAID Seminar, Santiago, Chile, January 2016
Tutorial: Introduction to Redex with Abstracting Abstract Machines
University of Chile, PLEAID Seminar, Santiago, Chile, January 2016
Verification and Refutation of Behavioral Contracts with Higher-Order Symbolic Execution
Johns Hopkins University, PL Seminar, Baltimore, Maryland, October 2015
Young Researcher Panel
ACM SIGPLAN Programming Languages Mentoring Workshop at ICFP, Vancouver, British Columbia, August 2015
Abstracting Abstract Machines
PLT Redex Summer School, University of Utah, Salt Lake City, Utah, July 2015
Verification and Refutation of Behavioral Contracts with Higher-Order Symbolic Execution
PL Wonks Seminar, Indiana University, Bloomington, Indiana, January 2015
Synthesis from Contracts
Defense Advanced Research Projects Agency, Arlington, Virginia, March 2014
Program Analysis for Trustworthy Software
Laboratory for Telecommunication Sciences, College Park, Maryland, March 2014
Soft Contract Verification
The ACM SIGPLAN International Conference on Functional Programming, Gothenborg, Sweden, September 2014
Soft Contract Verification
Dagstuhl Seminar on Scripting Languages and Frameworks: Analysis and Verification, Schloss Dagstuhl, Germany, July 2014
Analysis for Trustworthy Software
Third Annual Maryland Cybersecurity Center Symposium, College Park, Maryland, June 2014
Soft Contract Verification
NII Workshop on Software Contracts for Communication, Monitoring, and Security, Shonan Village, Japan, May 2014
From Principles to Practice with Class
Trends in Functional Programming in Education, Provo, Utah, May 2013
Abstracting Definitional Interpreters
Mid-Atlantic Programming Languages Seminar, College Park, Maryland, April 2013
Analysis for Trustworthy Software
Computer Science Colloquium, University of Maryland, College Park, Maryland, March 2013
Towards Verification of Behavioral Software Contracts
Microsoft Research, Research in Software Engineering, Redmond, Washington, November 2012
Raising the Level of Discourse with GnoSys
DARPA Clean-slate design of Resilient, Adaptive, Secure Hosts (CRASH) PI Meeting, San Diego, California, November 2012
Higher-Order Symbolic Execution via Contracts
The ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’12), Tuscon, Arizona, October 2012
Scalable Abstractions for Trustworthy Software
DARPA Automated Program Analysis for Cybersecurity (APAC) PI Meeting, Arlington, Virginia, October 2012
Verification via Abstract Reduction Semantics
PL Seminar, Aarhus University, Aarhus, Denmark, December 2011
Low-level Analysis for High-level Assurance
GnoSys project report for DARPA, Northeastern University, Boston, September 2011
The Complexity of kCFA
NII Workshop on Automated Techniques for Higher-Order Program Verification, Shonan Village, Japan, September 2011
Abstract Reduction Semantics
NII Workshop on Automated Techniques for Higher-Order Program Verification, Shonan Village, Japan, September 2011
So you’ve ruined your life: What comes after a PhD?
Northeastern CCIS PhD Seminar, Boston, Massachusetts, July 2011
An Object-Oriented World
RacketCon, Boston, Massachusetts, July 2011
What Program Analysis Can and Cannot Do for You
Computer Science Colloquium, Rice University, March 2011
What Program Analysis Can and Cannot Do for You
Computer Science Colloquium, University of Utah, Salt Lake City, Utah, February 2011
The Paradox of Flow Analysis, Or: What We Talk About When We Talk About Higher-Order Flow Analysis
PL Seminar, MIT, Cambridge, Massachusetts, February 2011
Modular Analysis via Abstract Reduction Semantics
New Jersey Programming Languages and Systems Seminar, Rutgers University, New Jersey, December 2010
Abstracting Abstract Machines
The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), Baltimore, Maryland, September 2010
Pushdown Control Flow Analysis
IBM Programming Languages Day, Hawthorne, New York, July 2010
Abstracting Abstract Machines: Storing and Stacking Continuations
Harvard Programming Languages Seminar, Cambridge, Massachusetts, July 2010
Resolving and Exploiting the k-CFA Paradox
The ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI 2010), Toronto, Ontario, June 2010
Abstracting Abstract Machines
New England Programming Languages and Systems Symposium, Yale University, New Haven, Connecticut, April 2010
Resolving and Exploiting the k-CFA Paradox
Computer and Information Science Colloquium, University of Oregon, Eugene, Oregon, April 2010
Resolving and Exploiting the k-CFA Paradox
New England Programming Languages and Systems Symposium, MIT, Cambridge, Massachusetts, December 2009
Subcubic Control-Flow Analysis Algorithms
Symposium in Honor of Mitchell Wand, Northeastern University, Boston, Massachusetts, August 2009
The Complexity of Flow Analysis in Higher-Order Languages
PhD dissertation defense, Brandeis University, Waltham, Massachussets, July 2009
Complexity of Flow Analysis
New England Programming Languages and Systems Symposium, Harvard University, Cambridge, Massachussets, November 2008
Deciding kCFA is complete for EXPTIME
The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), Victoria, British Columbia, September 2008
Flow analysis, Linearity, and PTIME
The 15th International Static Analysis Symposium (SAS 2008), Valencia, Spain, July 2008
Relating Complexity and Precision in Control Flow Analysis
The 12th ACM SIGPLAN International Conference on Functional Programming (ICFP 2007), Freiburg, Germany, October 2007
Relating Complexity and Precision in Control Flow Analysis
Northeastern Programming Languages Seminar, Boston, Massachusetts, May 2007
From Syntactic Sugar to the Syntactic Meth Lab: Using Macros to Cook the Language You Want
CoSci 21b (SICP), Brandeis University, Waltham, Massachusetts, December 2006
Linearity and Program Analysis, and Relating complexity and precision of approximation in control flow analysis
PL Seminar, Jr., Northeastern University, Boston, Massachusetts, October 2006
Algorithmic Trace Effect Analysis
MS thesis defense, University of Vermont, Burlington, Vermont, March 2006
Abstract Machines for the Multi-return λ-calculus
G711 (“Principles of Programming Languages”), Northeastern University, Boston, Massachusetts, December 2005
Algorithmic Trace Effect Analysis
Computer Science Research Day, University of Vermont, Burlington, Vermont, August 2005
Context Based Security in Programming Languages
Vermont EPSCoR annual conference, Burlington, Vermont, August 2005