David Van Horn

Research interests

I am interested in all aspects of program analysis and its applications to programming languages, software engineering, verification, and security. Specifically, I work toward enabling the production of software that can be mechanically reasoned about, with the ultimate goal of making the construction of reusable, trusted software components possible and effective. My research has spanned program analysis, semantics, and transformation, both in functional and object-oriented contexts; verification and model-checking; security; logic; complexity; and algorithms.

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 whenever 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.

  This work is supported by the National Science Foundation, Software and Hardware Foundations program.

• 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 and distributed video games in Racket. Available for pre-order from No Starch Press and Amazon. Written with Matthias Felleisen, Conrad Barski, and a group of Northeastern undergraduate students: Forrest Bice, Rose DeMaio, Spencer Florence, Feng-Yun Mimi Lin, Scott Lindeman, Nicole Nussbaum, Eric Peterson, and Ryan Plessner.

Activities

• ESOP: 2014 European Symposium on Programming, Program committee
• TFP: 2014 Trends in Functional Programming, Program committee
• HOPA: 2013 Workshop on Higher-Order Program Analysis, Program committee
• SCALA: 2013 Scala Workshop, Program committee
• ICFP: 2013-2016 International Conference on Functional Programming, Steering committee
• 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

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

In submission

Sound and Precise Malware Analysis for Android via Pushdown Reachability and Entry-Point Saturation. With Shuying Liang, Andrew W. Keep, and Matthew Might.
In submission to ACM Conference on Computer and Communications Security, 2013.
[ PDF ]

Correctly Optimizing Abstract Abstract Machines. With J. Ian Johnson, Nicholas Labich, and Matthew Might.
In submission to ACM International Conference on Functional Programming, 2013.
[ arXiv ]

Introspective pushdown analysis. With Christopher Earl, Ilya Sergey, J. Ian Johnson, and Matthew Might.
Invited to submission to Best of ICFP 2012 issue of Journal of Functional Programming, 2013.
[ PDF ]

AnaDroid: Malware Analysis of Android with User-supplied Predicates. With Shuying Liang and Matthew Might.
In submission to Workshop on Tools for Automatic Program Analysis, 2013.
[ PDF ]

Concrete Semantics for Pushdown Analysis: The Essence of Summarization. With Ian Johnson.
In submission to Workshop on Higher-Order Program Analysis.
[ PDF ]

Preprints

Pushdown Exception-Flow Analysis of Object-Oriented Programs. With Shuying Liang, Matthew Might, and Thomas Gilray.
[ arXiv ]

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

Publications

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

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.
[ PDF | Abstract | 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.
Invited to Best of ICFP 2012 special issue of JFP.
[ PDF | Abstract | ACM | arXiv ]

Systematic Abstraction of Abstract Machines. With Matthew Might.
Journal of Functional Programming, 22(4-5). September, 2012.
Best of ICFP 2010.
[ PDF | Abstract | CUP | 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

• From Principles to Practice with Class in the First Year, 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, 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, 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, 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, Decembe, 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, J. Ian Johnson, Andrew W. Keep, Nicholas Labich, Shuying Liang, Harry Mairson, Jan Midtgaard, Matthew Might, Ilya Sergey, Olin Shivers, Christian Skalka, Yannis Smaragdakis, Scott Smith, Sam Tobin-Hochstadt, and Mitchell Wand.