1,205 papers · page 7 of 61
Abhinav Jangda, Uday Bondhugula
Effective models for fusion of loop nests continue to remain a challenge in both general-purpose and domain-specific language (DSL) compilers. The difficulty often arises from the combinatorial explosion of grouping choices and their interaction with parallelism and locality. Thi…
Yue Li, Tian Tan, Anders Møller, Yannis Smaragdakis
Context sensitivity is an essential technique for ensuring high precision in static analyses. It has been observed that applying context sensitivity partially, only on a select subset of the methods, can improve the balance between analysis precision and speed. However, existing …
Leandro T. C. Melo, Rodrigo Geraldo Ribeiro, Breno Campos Ferreira Guimarães, Fernando Magno Quintão Pereira
Type inference is a feature that is common to a variety of programming languages. While, in the past, it has been prominently present in functional ones (e.g., ML and Haskell), today, many object-oriented/multi-paradigm languages such as C# and C++ offer, to a certain extent, suc…
Praveen Narayanan, Chung-chieh Shan
Disintegration is a relation on measures and a transformation on probabilistic programs that generalizes density calculation and conditioning, two operations widely used for exact and approximate inference. Existing program transformations that find a disintegration or density au…
Alex Simpson, Niels F. W. Voorneveld
The article investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural propert…
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
Capability machines provide security guarantees at machine level which makes them an interesting target for secure compilation schemes that provably enforce properties such as control-flow correctness and encapsulation of local state. We provide a formalization of a representativ…
Matías Toro, Ronald Garcia, Éric Tanter
No abstract available.
Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, Tom Schrijvers
Consistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by Siek and Taha serves as a guideline for designing gradual type systems with subtyping. Polymorphic types à la System F also induce a subtyping relation that rela…
David Zhao, Pavle Subotic, Bernhard Scholz
Logic programming languages such as Datalog have become popular as Domain Specific Languages (DSLs) for solving large-scale, real-world problems, in particular, static program analysis and network analysis. The logic specifications that model analysis problems process millions of…
Leif Andersen, Vincent St-Amour, Jan Vitek, Matthias Felleisen
While high-level languages come with significant readability and maintainability benefits, their performance remains difficult to predict. For example, programmers may unknowingly use language features inappropriately, which cause their programs to run slower than expected. To ad…
Emery D. Berger, Celeste Hollenbeck, Petr Maj, Olga Vitek, Jan Vitek
In a 2014 article, Ray, Posnett, Devanbu, and Filkov claimed to have uncovered a statistically significant association between 11 programming languages and software defects in 729 projects hosted on GitHub. Specifically, their work answered four research questions relating to sof…
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady
We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of non-recursive programs. First, we apply ranking functions to re…
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Prateesh Goyal, Rasmus Ibsen-Jensen, Andreas Pavlogiannis
Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, and so on. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where t…
Tiago Cogumbreiro, Raymond Hu, Francisco Martins, Nobuko Yoshida
We present Armus, a verification tool for dynamically detecting or avoiding barrier deadlocks. The core design of Armus is based on phasers, a generalisation of barriers that supports split-phase synchronisation, dynamic membership, and optional-waits. This allows Armus to handle…
Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
We prove that the observational equivalence problem for a finitary fragment of the programming langauge ML is recursively equivalent to the reachability problem for extended branching vector addition systems with states (EBVASS). This result has two natural and independent parts.…
Leandro Facchinetti, Zachary Palmer, Scott F. Smith
Developing accurate and efficient program analyses for languages with higher-order functions is known to be difficult. Here we define a new higher-order program analysis, Demand-Driven Program Analysis (DDPA), which extends well-known demand-driven lookup techniques found in firs…
David Grove, Sara S. Hamouda, Benjamin Herta, Arun Iyengar, Kiyokuni Kawachiya, Josh Milthorpe, Vijay A. Saraswat, Avraham Shinnar + 2 more
Cloud computing has made the resources needed to execute large-scale in-memory distributed computations widely available. Specialized programming models, e.g., MapReduce, have emerged to offer transparent fault tolerance and fault recovery for specific computational patterns, but…
Matthew Hague, Anthony W. Lin, Chih-Duo Hong
Minification is a widely accepted technique that aims at reducing the size of the code transmitted over the web. This article concerns the problem of semantic-preserving minification of Cascading Style Sheets (CSS)—the de facto language for styling web documents—based on merging …
Nicholas Jacek, Meng-Chieh Chiu, Benjamin M. Marlin, J. Eliot B. Moss
We consider the ultimate limits of program-specific garbage collector (GC) performance for real programs. We first characterize the GC schedule optimization problem. Based on this characterization, we develop a linear-time dynamic programming solution that, given a program run an…
Minseok Jeon, Sehun Jeong, Sung Deok Cha, Hakjoo Oh
We present a new machine-learning algorithm with disjunctive model for data-driven program analysis. One major challenge in static program analysis is a substantial amount of manual effort required for tuning the analysis performance. Recently, data-driven program analysis has em…