46 citations · 222 across the 24 of their papers we have counts for
25 papers
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Cameron Moy, Phúc C. Nguyen, Sam Tobin-Hochstadt +1
Gradually-typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks at the boundaries betwe…
A Vision for Online Verification-Validation
Matthew A. Hammer, Bor-Yuh Evan Chang, David Van Horn
Today's programmers face a false choice between creating software that is extensible and software that is correct. Specifically, dynamic languages permit software that is richly ex…
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory
David Darais, David Van Horn
Galois connections are a foundational tool for structuring abstraction in semantics and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of…
Higher-order symbolic execution for contract verification and refutation
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
We present a new approach to automated reasoning about higher-order programs by endowing symbolic execution with a notion of higher-order, symbolic values. Our approach is sound an…
Pushdown Control-Flow Analysis for Free
Thomas Gilray, Steven Lyde, Michael D. Adams +2
Traditional control-flow analysis (CFA) for higher-order languages, whether implemented by constraint-solving or abstract interpretation, introduces spurious connections between ca…
Running Probabilistic Programs Backwards
Neil Toronto, Jay McCarthy, David Van Horn
Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other…
Relatively Complete Counterexamples for Higher-Order Programs
Phuc C. Nguyen, David Van Horn
In this paper, we study the problem of generating inputs to a higher-order program causing it to error. We first study the problem in the setting of PCF, a typed, core functional l…
Galois Transformers and Modular Abstract Interpreters
David Darais, Matthew Might, David Van Horn
The design and implementation of static analyzers has become increasingly systematic. Yet for a given language or analysis feature, it often requires tedious and error prone work t…
Pruning, Pushdown Exception-Flow Analysis
Shuying Liang, Weibin Sun, Matthew Might +2
Statically reasoning in the presence of exceptions and about the effects of exceptions is challenging: exception-flows are mutually determined by traditional control-flow and point…
Flow analysis, linearity, and PTIME
David Van Horn, Harry G. Mairson
Flow analysis is a ubiquitous and much-studied component of compiler technology---and its variations abound. Amongst the most well known is Shivers' 0CFA; however, the best known a…
Deciding CFA is complete for EXPTIME
David Van Horn, Harry G. Mairson
We give an exact characterization of the computational complexity of the CFA hierarchy. For any , we prove that the control flow decision problem is complete for determin…
The Complexity of Flow Analysis in Higher-Order Languages
David Van Horn
This dissertation proves lower bounds on the inherent difficulty of deciding flow analysis problems in higher-order programming languages. We give exact characterizations of the co…
Resolving and Exploiting the -CFA Paradox
Matthew Might, Yannis Smaragdakis, David Van Horn
Low-level program analysis is a fundamental problem, taking the shape of "flow analysis" in functional languages and "points-to" analysis in imperative and object-oriented language…
Sound and Precise Malware Analysis for Android via Pushdown Reachability and Entry-Point Saturation
Shuying Liang, Andrew W. Keep, Matthew Might +4
We present Anadroid, a static malware analysis framework for Android apps. Anadroid exploits two techniques to soundly raise precision: (1) it uses a pushdown system to precisely m…
AnaDroid: Malware Analysis of Android with User-supplied Predicates
Shuying Liang, Matthew Might, David Van Horn
Today's mobile platforms provide only coarse-grained permissions to users with regard to how third- party applications use sensitive private data. Unfortunately, it is easy to disg…
Soft Contract Verification
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
Behavioral software contracts are a widely used mechanism for governing the flow of values between components. However, run-time monitoring and enforcement of contracts imposes sig…
From Principles to Practice with Class in the First Year
Sam Tobin-Hochstadt, David Van Horn
We propose a bridge between functional and object-oriented programming in the first-year curriculum. Traditionally, curricula that begin with functional programming transition to a…
Abstracting Abstract Control (Extended)
J. Ian Johnson, David Van Horn
The strength of a dynamic language is also its weakness: run-time flexibility comes at the cost of compile-time predictability. Many of the hallmarks of dynamic languages such as c…
Optimizing Abstract Abstract Machines
J. Ian Johnson, Nicholas Labich, Matthew Might +1
The technique of abstracting abstract machines (AAM) provides a systematic approach for deriving computable approximations of evaluators that are easily proved sound. This article…
Pushdown Abstractions of JavaScript
David Van Horn, Matthew Might
We design a family of program analyses for JavaScript that make no approximation in matching calls with returns, exceptions with handlers, and breaks with labels. We do so by start…
Higher-Order Symbolic Execution via Contracts
Sam Tobin-Hochstadt, David Van Horn
We present a new approach to automated reasoning about higher-order programs by extending symbolic execution to use behavioral contracts as symbolic values, enabling symbolic appro…
Evaluating Call-By-Need on the Control Stack
Stephen Chang, David Van Horn, Matthias Felleisen
Ariola and Felleisen's call-by-need λ-calculus replaces a variable occurrence with its value at the last possible moment. To support this gradual notion of substitution, function a…
Stack-Summarizing Control-Flow Analysis of Higher-Order Programs
Christopher Earl, Matthew Might, David Van Horn
Two sinks drain precision from higher-order flow analyses: (1) merging of argument values upon procedure call and (2) merging of return values upon procedure return. To combat the…
Pushdown Control-Flow Analysis of Higher-Order Programs
Christopher Earl, Matthew Might, David Van Horn
Context-free approaches to static analysis gain precision over classical approaches by perfectly matching returns to call sites---a property that eliminates spurious interprocedura…