Refactoring is a code transformation performed at development time that improves the quality of code while preserving its observable behavior. Macro expansion is also a code transformation, but performed at compile time, that replaces instances of macro invocation patterns with the corresponding macro body or template. The key insight of this paper is that for each pattern-template macro, we can automatically generate a corresponding refactoring tool that finds complex code fragments matching the macro template and replaces them with the equivalent but simpler macro invocation pattern; we call this novel refactoring process macrofication. Conceptually, macrofication involves running macro expansion in reverse; however, it does require a more sophisticated pattern matching algorithm and additional checks to ensure that the refactoring always preserves program behavior. We have implemented a macrofication tool for a hygienic macro system in JavaScript, integrated it into a development environment and evaluated it by refactoring a popular open source JavaScript library. Results indicate that it is sufficiently flexible for complex refactoring and thereby enhances the development workflow while scaling well even for larger code bases.

Multithreaded programs are notoriously prone to unintended interference between concurrent threads. To address this problem, we argue that yield annotations in the source code should document all thread interference, and we present a type system for verifying the absence of undocumented interference in Java programs. Under this type system, well-typed programs behave as if context switches occur only at yield annotations. Thus, well-typed programs can be understood using intuitive sequential reasoning, except where yield annotations remind the programmer to account for thread interference.

The key idea of game semantics is that a term can interact with its enclosing context via various events, such as function calls and returns. A trace is a sequence of such interaction events. The meaning of the term is then naturally represented by the set of all event traces that the term can generate. Game semantics allows us to define the meaning of both expressions and types in the same domain which enables an interesting alternative to subject reduction for proving type soundness. This paper uses game semantics to define the meaning of and verify type soundness for a sequence of programming languages, starting with a functional sequential language (the call-by-value simply-typed lambda calculus), and then extending that proof with sub typing, side effects, control effects, and concurrency. These proofs are reasonably short and fairly semantic in structure, focusing on the relationship between the meanings of each term and its corresponding type. In particular, we show that the typing and sub typing relations are both conservative approximations of alternating trace containment.

Lisp and Scheme have demonstrated the power of macros to enable programmers to evolve and craft languages. In languages with more complex syntax, macros have had less success. In part, this has been due to the difficulty in building expressive hygienic macro systems for such languages. JavaScript in particular presents unique challenges for macro systems due to ambiguities in the lexing stage that force the JavaScript lexer and parser to be intertwined. In this paper we present a novel solution to the lexing ambiguity of JavaScript that enables us to cleanly separate the JavaScript lexer and parser by recording enough history during lexing to resolve ambiguities. We give an algorithm for this solution along with a proof that it does in fact correctly resolve ambiguities in the language. Though the algorithm and proof we present is specific to JavaScript, the general technique can be applied to other languages with ambiguous grammars. With lexer and parser separated, we then implement an expressive hygienic macro system for JavaScript called sweet.js.

In this paper we present a new tool called DOCaT (Dynamic Object Capability Tracer), a model checker for JavaScript that detects capability leaks in an object capability system. DOCaT includes an editor that highlights the sections of code that can be potentially transferred to untrusted third-party code along with a trace showing how the code could be leaked in an actual execution. This code highlighting provides a simple way of visualizing the references untrusted code potentially has access to and helps programmers to discover if their code is leaking more capabilities then required. DOCaT is implemented using a combination of source code rewriting (using Sweet.js, a JavaScript macro system), dynamic behavioral intercession (Proxies, introduced in ES6, the most recent version of JavaScript), and model checking. Together these methods are able to locate common ways for untrusted code to elevate its authority.

We present a novel and lightweight library-based approach to symbolic execution based on a peer architecture. Rather than defining a new interpreter or compiler to build a symbolic execution engine for a particular language, we simply use the existing features of the language so that the engine works as a peer of the target program. Our approach is based on the insight that languages that provide the ability to dynamically dispatch primitive operations (e.g. many scripting languages such as Python) allow us to track symbolic values at runtime. We present an architecture and implementation of our peer architecture in Python and discuss results of running our symbolic execution engine on several well known algorithms and data structures.

The potential for unexpected interference between threads makes multithreaded programming notoriously difficult. Programmers use a variety of synchronization idioms such as locks and barriers to restrict where interference may actually occur. Unfortunately, the resulting actual interference points are typically never documented and must be manually reconstructed as the first step in any subsequent programming task (code review, refactoring, etc). This paper proposes explicitly documenting actual interference points in the program source code, and it presents a type and effect system for verifying the correctness of these interference specifications. Experimental results on a variety of Java benchmarks show that this approach provides a significant improvement over prior systems based on method-level atomicity specifications. In particular, it reduces the number of interference points one must consider from several hundred points per thousand lines of code to roughly 13 per thousand lines of code. Explicit interference points also serve to highlight all known concurrency defects in these benchmarks.

This paper focuses on extensibility, the ability of a programmer using a particular language to extend the expressiveness of that language. This paper explores how to provide an interesting notion of extensibility by virtualizing the interface between code and data. A virtual value is a special value that supports behavioral intercession. When a primitive operation is applied to a virtual value, it invokes a trap on that virtual value. A virtual value contains multiple traps, each of which is a user-defined function that describes how that operation should behave on that value. This paper formalizes the semantics of virtual values, and shows how they enable the definition of a variety of language extensions, including additional numeric types; delayed evaluation; taint tracking; contracts; revokable membranes; and units of measure. We report on our experience implementing virtual values for Javascript within an extension for the Firefox browser.

We present a method to support the gradual evolution of secure scripts by formalizing an extension of the simply-typed lambda calculus that provides information flow constructs. These constructs allow initially insecure programs to evolve via targeted refactoring and to provide dynamic information flow guarantees via casts, as well as static information flow guarantees via labeled types.

Behavioral contracts are embraced by software engineers because they document module interfaces, detect interface violations, and help identify faulty modules (packages, classes, functions, etc). This paper extends prior higher-order contract systems to also express and enforce temporal properties, which are common in software systems with imperative state, but which are mostly left implicit or are at best informally specified. The paper presents both a programmatic contract API as well as a temporal contract language, and reports on experience and performance results from implementing these contracts in Racket. Our development formalizes module behavior as a trace of events such as function calls and returns. Our contract system provides both non-interference (where contracts cannot influence correct executions) and also a notion of completeness (where contracts can enforce any decidable, prefix-closed predicate on event traces).

We have created a content-based image retrieval framework for computed tomography images of pulmonary nodules. When presented with a nodule image, the system retrieves images of similar nodules from a collection prepared by the Lung Image Database Consortium (LIDC). The system (1) extracts images of individual nodules from the LIDC collection based on LIDC expert annotations, (2) stores the extracted data in a flat XML database, (3) calculates a set of quantitative descriptors for each nodule that provide a high-level characterization of its texture, and (4) uses various measures to determine the similarity of two nodules and perform queries on a selected query nodule. Using our framework, we compared three feature extraction methods: Haralick co-occurrence, Gabor filters, and Markov random fields. Gabor and Markov descriptors perform better at retrieving similar nodules than do Haralick co-occurrence techniques, with best retrieval precisions in excess of 88%. Because the software we have developed and the reference images are both open source and publicly available they may be incorporated into both commercial and academic imaging workstations and extended by others in their research.

Research studies have shown that advances in computed tomography (CT) technology allow better detection of pulmonary nodules by generating higher-resolution images. However, the new technology also generates many more individual transversal reconstructions, which as a result may affect the efficiency and accuracy of the radiologists interpreting these images. The goal of our research study is to build a content-based image retrieval (CBIR) system for pulmonary CT nodules. Currently, texture is used to quantify the image content, but any other image feature could be incorporated into the proposed system. Unfortunately, there is no texture model or similarity measure known to work best for encoding nodule texture properties or retrieving most similar nodules. Therefore, we investigated and evaluated several texture models and similarity measures with respect to nodule size, number of retrieved nodules, and radiologist agreement on the nodules' texture characteristic. The results were generated on 90 thoracic CT scans collected by the Lung Image Database Consortium (LIDC). Every case was annotated by up to four radiologists marking the contour of nodules and assigning nine characteristics (including texture) to each identified nodule. We found that Gabor texture descriptors produce the best retrieval results regardless of the nodule size, number of retrieved items or similarity metric. Furthermore, when analyzing the radiologists' agreement on the texture characteristic, we found that when just two radiologists agreed, the average precision increased from 88% to 96% for both Gabor and Markov texture features. Moreover, once three or four radiologists agreed the precision increased to nearly 100%.

Automatic liver segmentation from abdominal computed tomography (CT) images based on gray levels or shape alone is difficult because of the overlap in gray-level ranges and the variation in position and shape of the soft tissues. To address these issues, we propose an automatic liver segmentation method that utilizes low-level features based on texture information; this texture information is expected to be homogenous and consistent across multiple slices for the same organ. Our proposed approach consists of the following steps: first, we perform pixel-level texture extraction; second, we generate liver probability images using a binary classification approach; third, we apply a split-and-merge algorithm to detect the seed set with the highest probability area; and fourth, we apply to the seed set a region growing algorithm iteratively to refine the liver's boundary and get the final segmentation results. Furthermore, we compare the segmentation results from three different texture extraction methods (Co-occurrence Matrices, Gabor filters, and Markov Random Fields (MRF)) to find the texture method that generates the best liver segmentation. From our experimental results, we found that the co-occurrence model led to the best segmentation, while the Gabor model led to the worst liver segmentation. Moreover, co-occurrence texture features alone produced approximately the same segmentation results as those produced when all the texture features from the combined co-occurrence, Gabor, and MRF models were used. Therefore, in addition to providing an automatic model for liver segmentation, we also conclude that Haralick cooccurrence texture features are the most significant texture characteristics in distinguishing the liver tissue in CT scans.