David Van Horn

Research interests

My work supports scientific foundations for software construction and understanding. I am interested in the design, implementation, and use of programming languages. In particular, my research has focused on the analysis of higher-order programs and its complexity. I have proved novel upper and lower bounds for a number of important program analyses and used these insights to design better program analyzers. I have also developed type systems for inferring and verifying temporal models of programs.

Current projects

• Scalable and precise abstractions of programs for trustworthy software

  Applications deployed on mobile devices play a critical role in the fabric of daily life. They carry sensitive data and have capabilities with significant social and financial effect. Yet while it is paramount that such software is trustworthy, these applications pose challenges beyond the reach of current practice for low-cost, high-assurance verification and analysis. The primary goal of this project is to enable sound, secure, automatic program analysis for the elimination of security vulnerabilities in mobile applications written in high-level programming languages.

  This work is supported by the DARPA Information Innovation Office, Automated Program Analysis for Cybersecurity program.

• Behavioral software contract verification

  Behavioral software contracts express invariants and agreements between components of a program (procedures, modules, classes, even different languages) and assign blame to the appropriate party whenver these agreements are violated. As such, contracts form a rich specification language, allowing arbitrary properties to be encoded a programs. This richness is crucial for constructing reliable components, however the expressivity of contracts thwarts static reasoning and incurs significant run-time monitoring costs. This work rectifies the situation by providing foundations for modular and compositional automated reasoning about behavioral contracts.

• Raising the level of discourse with GnoSys

  The main thesis of this project is that by making language mechanisms available to programmers that capture more design knowledge, this knowledge can be leveraged to qualitatively improve automated reasoning about programs. As part of the GnoSys project, I am investigating the interaction of analysis with language design, formal methods, and operating systems to enable mutually beneficial combinations for constructing robust systems. The focus of my work is to design program analysis tools for capturing domain knowledge and to design program abstractions that can be exploited by the components of the system such as the operating system and automated theorem prover.

  This work is supported by the DARPA Clean-slate design of Resilient, Adaptive, Secure Hosts (CRASH) program.

• Realm of Racket

  This book explores programming interactive video games in Racket. To be published by No Starch Press. Written with Matthias Felleisen, Conrad Barski, and The Roquets, a group of Northeastern undergraduate students.

Activities

• POPL: 2013 Symposium on Principles of Programming Languages, External review committee
• TFP: 2012 Symposium on Trends in Functional Programming, Program committee
• ICFP: 2011 International Conference on Functional Programming, Program committee
• NII: Workshop on Automated Techniques for Higher-Order Program Verification, Organizer
• NEPLS: New England Programming Languages and Systems Symposium, Spring 2011, Chair
• SFP: 2011 Scheme and Functional Programming Workshop, Program committee
• HOFA: Higher-Order Flow Analysis Forum, Moderator
• SRFI: Scheme Requests for Implementation, Editor

Teaching

• CSU2500: Introduction to Programming and Computing I (Regular & Honors)
• CSU2510: Introduction to Programming and Computing II (Regular)
• CSU2510: Introduction to Programming and Computing II (Honors)

I believe understanding computation to be a basic component of literacy. Many of my students have not only mastered this aspect of literacy, they teach it! Dozens of my students have gone on to teach middle school students in the Boston area as part of the Bootstrap program, which empowers students to program their own video games using purely algebraic and geometric concepts.

Papers

Preprints

Pushdown Abstractions of JavaScript. With Matthew Might.
[ PDF | Abstract | arXiv ]

Abstract Reduction Semantics for Modular Higher-Order Contract Verification. With Sam Tobin-Hochstadt.
[ PDF | Abstract | arXiv ]

Publications

Systematic Abstraction of Abstract Machines. With Matthew Might.
Accepted with minor revisions, Journal of Functional Programming. To appear, 2012.
[ PDF | Abstract | arXiv ]

Abstracting Abstract Machines. With Matthew Might.
Communications of the ACM, Research Highlights, 54(9), September 2011.
[ PDF | Abstract | 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.
[ PDF | Abstract | 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.
[ PDF | Abstract | arXiv ]

Abstracting Abstract Machines. With Matthew Might.
The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP'10), Baltimore, Maryland, September, 2010.
[ PDF | Abstract | 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, Canada, August, 2010.
[ PDF | Abstract | 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.
Best student paper award.
[ PDF | Abstract | 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.
[ PDF | Abstract | ACM ]

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

Subcubic Control Flow Analysis Algorithms. With Jan Midtgaard.
Roskilde Unversitet, Computer science research report #125, May 2009. Presented at the Symposium in Honor of Mitchell Wand. Accepted to appear in revised form in the journal Higher-Order and Symbolic Computation.
[ PDF | Abstract | RUC ]

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.
[ PDF | Abstract | ACM ]

A Few Principles of Macro Design. With David Herman.
The ACM Workshop on Scheme and Functional Programming, Victoria, British Columbia, Canada, September 2008.
[ PDF | Abstract | WSFP ]

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

Types and Trace Effects of Higher Order Programs. With Christian Skalka and Scott Smith.
Journal of Functional Programming, 18(2), March 2008.
[ PDF | Abstract | 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.
[ PDF | Abstract | ACM ]

Algorithmic Trace Effect Analysis.
MS thesis, University of Vermont, 2006.
[ PDF | Abstract | UVM ]

A Type and Effect System for Flexible Abstract Interpretation of Java. With Christian Skalka and Scott Smith.
The ACM Workshop on Abstract Interpretations of Object-Oriented Programs, Electronic Notes in Theoretical Computer Science, Volume 131. January 2005.
[ PDF | Abstract | Elsevier ]

Talks

• 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, University of Utah, Salt Lake City, February, 2011.
• The Paradox of Flow Analysis, Or: What We Talk About When We Talk About Higher-Order Flow Analysis, 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, The 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, 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, December 2009.
• Subcubic Control-Flow Analysis Algorithms, Symposium in Honor of Mitchell Wand, Northeastern University, Boston, August 2009.
• The Complexity of Flow Analysis in Higher-Order Languages, PhD dissertation defense, Brandeis University, Waltham, July 2009.
• Complexity of Flow Analysis, New England Programming Languages and Systems Symposium, Harvard University, Cambridge, November 2008.
• Deciding kCFA is complete for EXPTIME, The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), Victoria, British Columbia, Canada, September, 2008.
• Flow analysis, Linearity, and PTIME, The 15th International Static Analysis Symposium (SAS 2008), Valencia, Spain, July, 2008.
• Linear Logic and the Complexity of Control Flow Analysis, CMU Principles of Programming Seminar, January 2008 (presented by Harry Mairson).
• 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, May, 2007.
• Relating Complexity and Precision in Control Flow Analysis, IBM Programming Languages Day, Hawthorne, New York, May, 2007.
• From Syntactic Sugar to the Syntactic Meth Lab: Using Macros to Cook the Language You Want, Brandeis University, CoSci 21b, December, 2006.
• Linearity and Program Analysis, and Relating complexity and precision of approximation in control flow analysis, Northeastern University PL Seminar, Jr., October, 2006.
• Proofnets and Paths in Constructive Classical Logic: Too Old, Too New, (presented by Harry Mairson) Geometry of Interaction Workshops, Marseille, February 2006.
• Algorithmic Trace Effect Analysis, MS thesis defense, University of Vermont, March 2006. Available in hard copy from the Bailey/Howe library at UVM.
• Abstract Machines for the Multi-return λ-calculus, presented to Northeastern University G711 ("Principles of Programming Languages"), December 2005.
• Algorithmic Trace Effect Analysis, presented to the University of Vermont Computer Science Research Day, August 2005. Research poster.
• Context Based Security in Programming Languages, presented to Vermont EPSCoR annual conference. August 2005.

Collaborators

Stephen Chang, Christopher Earl, Matthias Felleisen, David Herman, Harry Mairson, Jan Midtgaard, Matthew Might, Olin Shivers, Christian Skalka, Yannis Smaragdakis, Scott Smith, Sam Tobin-Hochstadt, and Mitchell Wand.