Projects
Gradual Verification: From Scripting to Proving (PI)
Programmers are rapidly adopting expressive, dynamically typed, higher-order functional and object-oriented programming languages for their everyday development tasks. Over time, these programs are often fortified with static type checking by migrating programs using gradual types, a technique first developed in the research community, but now widely used by the largest industrial software development companies. Unfortunately, there are limits both to what properties gradual types can validate and the help they can provide programs as they engage in the migration process. In parallel, researchers have developed sophisticated next generation programming languages with integrated verification features. These languages are able to validate much stronger claims about the correctness of software, but their industrial adoption has lagged far behind gradual typing. Consequently, verification is not being integrated in the everyday lives of programmers and the quality and reliability of software suffers because of it. This represents a tremendous missed opportunity considering the rapid advancement of automated verification techniques.This project aims to provide foundational theories, pragmatic tools, and a pedagogical framework for closing the expressivity gap between the everyday languages of programmers and these verification-integrated languages, enabling pathways to verified programming at every point along the spectrum scripting languages to theorem proving languages.
This project is supported by the National Science Foundation CAREER program.
Online Verification-Validation (PI)
Increasingly, modern software on the web is richly extensible, accelerating its evolution and dramatically reducing the time between development and deployment. The intellectual merit of this research consists of challenging the false choice between creating software that is extensible (easy to reuse and extend) and software that is correct (meets its specifications). The new approach advanced by this work, Incremental Verification-Validation, enables programmers to bring domain-specific safely disciplines to extensible systems, by providing a framework where these disciplines are communicated both precisely and usefully, as executable code. The project's broader significance and importance consist in changing the way programmers approach building correct extensible software for the web. Incremental Verification-Validation encourages programmers to co-design their systems with executable specifications that check these systems dynamically, as they execute. Moreover, unlike typical assertions, which execute dynamically and non-incrementally, the proposed are subject to novel patterns that enhance their performance: In regressive validation, verification partially discharges some checks, dynamically rewriting the program with residual versions; in progressive verification, online verification occurs in passes that each cache and reuse work, to avoid from-scratch verification of facts that still hold from earlier passes. Finally, to avoid forcing analysis programmers to reason about incremental changes explicitly in each analysis that they create, the meta layer expresses incremental computations implicitly, using an implicitly-incremental meta language whose abstractions hide reasoning on a per-change basis.
This collaboration with Matthew Hammer and Bor-Yuh (Evan) Chang is
supported by the National Science Foundation Software and Hardware Foundations program.
The Science and Applications of Crypto-Currency (Co-PI)
Crypto-currencies and smart contracts are a new wave of disruptive technology that will shape the future of money and financial transactions. Today, crypto-currencies are a billion-dollar market, and hundreds of companies are entering this space, promising exciting new markets and eco-systems. Unfortunately, usage of crypto-currencies outstrips our understanding. Currently most crypto currencies rely on heuristic designs without a solid appreciation of the necessary security properties, or any formal basis upon which strong assurance of such properties might be achieved.This work aims to establish a rigorous scientific foundation for crypto-currencies. To achieve this, this work blends cryptography, game theory, programming languages, and systems security techniques. Expected outcomes include new crypto-currency designs with provable security properties, financially enforceable cryptographic protocols whose security properties are backed by enforceable payments in case of a breach, smart contract systems that are easy to program and formally verifiable, as well as high-assurance systems for storing and handling high-value crypto-currencies and transactions. The project will provide solutions to some of the most difficult and important technical questions surrounding the current digital-money revolution. The investigators will organize a crypto-currency speaker series that will bring together technologists, economists, social scientists, and policy-makers to foster collaborations that will shape the future of digital currencies.
This collaboration with Elaine Shi, Emin Sirer, Jonathan Katz, Dawn Song, and Michael Hicks is supported by the National Science Foundation Secure & Trustworthy Cyberspace program.
Sound Over- and Under-Approximation of Complexity and Information Security (Co-PI)
Our primary goal is to enable sound, highly automated program analysis for the elimination of complexity and side-channel vulnerabilities in applications for which only bytecode source is available.Toward this goal, we envision orders-of-magnitude improvements in scale, precision, and speed of algorithmic resource usage vulnerability analysis. The central thesis of our work is that these breakthroughs are achievable through an interplay of techniques to (1) quantify and compartmentalize adversary influence, (2) simultaneously box in resource usage analysis of a program from above using sound static analysis and below using dynamic analysis and symbolic exe- cution, and (3) integrate a human analyst in to the iterative refinement loop of the system to quickly confirm, dismiss, and focus hypotheses about resource usage.
This collaboration with Eric Koskinen, Dawn Song, and Michael Hicks is supported by the DARPA Information InnovationOffice, Space/Time Analysis for Cybersecurity program.
Trustworthy and Composable Software Systems with Contracts (PI)
Over the past decade, language-based security mechanisms—such
as type systems, model checkers, symbolic executors, and other program
analyses—have been successfully used to uncover or prevent many
important (exploitable) software vulnerabilities, such as buffer
overruns, side channels, unchecked inputs (leading to code injection),
and race conditions, among others. But despite significant advances,
current work makes two unrealistic assumptions: (1) the analyzed code
comprises a complete program (as opposed to a framework or set of
components), and (2) the software is written in a single programming
language. These assumptions ignore the reality of modern software,
which is composed of large sets of interacting components constructed
in several programming languages that provide varying degrees of
assurance that the components are well-behaved.
In this project, we aim to address these limitations by
developing new static-analysis techniques based on software contracts,
which provide a way to extend the analysis of components to reason
about security of an entire heterogeneous system.
This collaboration with Sam Tobin-Hochstadt, Jeff Foster, and
Michael Hicks, is supported by the National Security Agency, Science
of Security Research Lablet program.
Behavioral Software Contract Verification (Co-PI)
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. Such contracts tend to be
formulated in the full programming language, allowing arbitrary
properties to be encoded a programs. While this is crucial for
constructing reliable components, it thwarts static reasoning and
incurs significant run-time monitoring costs. This work rectifies the
situation with tools for modular and compositional automated reasoning
about behavioral contracts.
This collaboration with Sam Tobin-Hochstadt is supported by the
National Science Foundation, Software and Hardware Foundations
program.
Scalable and precise abstractions of programs for trustworthy software (PI)
Applications deployed on mobile devices play a critical role in our
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 in high-level
programming languages.
This collaboration with Matthew Might is supported by the DARPA Information Innovation Office, Automated Program Analysis for Cybersecurity program. Read more.
Raising the level of discourse with GnoSys (Senior personnel)
The goal of this project is to design language mechanisms that capture
design knowledge and to leverage this knowledge 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 collaboration with Matthias Felleisen, Matthew Flatt, Pete
Manolios, Matthew Might, Olin Shivers, and Mitchell Wand is supported
by the DARPA Clean-slate design of Resilient, Adaptive, Secure Hosts
(CRASH) program.
Students
Current
Past
- Phúc C. Nguyễn, Higher-order Symbolic Execution, Ph.D., UMD, 2019; now at Google
- Thomas Gilray, Post-doc at UMD; now asst. prof. at University of Alabama, Birmingham
- Niki Vazou, Post-doc at UMD; now asst. prof. at IMDEA
- Nicholas Labich, M.S., UMD, 2018
- David Darais, Mechanizing Abstract Interpretation, Ph.D., UMD, 2017; now an asst. prof. at University of Vermont
- Kristopher Micinski, Interaction-based Security for Mobile Apps, Ph.D., UMD, 2018 (Committee member); now a visiting asst. prof. at Haverford College
- Neil Toronto, post-doc at UMD; now at MSR, Cambridge
- Dionna Amalie Glaze, Automating Abstract Interpretation of Abstract Machines, Ph.D., Northeastern University, 2015; now at Google
- Vincent St-Amour, How to Generate Actionable Advice about Performance Problems, Ph.D., Northeastern University, 2015 (Committee member)
- Piotr Mardziel, Modeling, Measuring, and Limiting Adversary Knowledge, Ph.D., University of Maryland, 2015 (Committee member)
- Stephen Chang, On the Relation Between Laziness and Strictness, Ph.D., Northeastern University, 2014 (Committee member)
- Shuying Liang, Static Analysis of Android Applications, Ph.D., University of Utah, 2014 (Committee member)
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
