1,971 papers · page 13 of 99
Ariel E. Kellison, Justin Hsu
Algorithms operating on real numbers are implemented as floating-point computations in practice, but floating-point operations introduce roundoff errors that can degrade the accuracy of the result. We propose Λnum, a functional programming language with a type system that can exp…
Ameya Ketkar, Daniel Ramos, Lazaro Clapp, Raj Barik, Murali Krishna Ramanathan
In today's software industry, large-scale, multi-language codebases are the norm. This brings substantial challenges in developing automated tools for code maintenance tasks such as API migration or dead code cleanup. Tool builders often find themselves caught between two less-th…
Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
Symmetry reduction (SR) and partial order reduction (POR) aim to scale up model checking by exploiting the underlying program structure: SR avoids exploring executions equivalent up to some permutation of symmetric threads, while POR avoids exploring executions equivalent up to r…
Bastian Köpcke, Sergei Gorlatch, Michel Steuwer
Graphics Processing Units (GPU) offer tremendous computational power by following a throughput oriented paradigm where many thousand computational units operate in parallel. Programming such massively parallel hardware is challenging. Programmers must correctly and efficiently co…
Aleksandar Krastev, Nikola Samardzic, Simon Langowski, Srinivas Devadas, Daniel Sánchez
Fully Homomorphic Encryption (FHE) enables computing on encrypted data, letting clients securely offload computation to untrusted servers. While enticing, FHE has two key challenges that limit its applicability: it has high performance overheads (10,000× over unencrypted computat…
Avery Laird, Bangtian Liu, Nikolaj S. Bjørner, Maryam Mehri Dehnavi
We present SpEQ, a quick and correct strategy for detecting semantics in sparse codes and enabling automatic translation to high-performance library calls or domain-specific languages (DSLs). When sparse linear algebra codes contain implicit preconditions about how data is stored…
Mathias Rud Laursen, Wenyuan Xu, Anders Møller
Static program analysis for JavaScript is more difficult than for many other programming languages. One of the main reasons is the presence of dynamic property accesses that read and write object properties via dynamically computed property names. To ensure scalability and precis…
Yuxiang Lei, Camille Bossut, Yulei Sui, Qirun Zhang
Context-free language reachability (CFL-reachability) is a prominent model for formulating program analysis problems. Almost all CFL-reachability algorithms are based on the Reps-Horwitz-Sagiv (RHS) tabulation. In essence, the RHS tabulation, based on normalized context-free gram…
Dorian Lesbre, Matthieu Lemerre
Rewriting and static analyses are mutually beneficial techniques: program transformations change the intensional aspects of the program, and can thus improve analysis precision, while some efficient transformations are enabled by specific knowledge of some program invariants. Des…
Shaohua Li, Theodoros Theodoridis, Zhendong Su
We introduce a novel approach for testing optimizing compilers with code from real-world applications. The main idea is to construct well-formed programs by fusing multiple code snippets from various real-world projects. The key insight is backed by the fact that the large volume…
Jianlin Li, Eric Wang, Yizhou Zhang
A key promise of probabilistic programming is the ability to specify rich models using an expressive program- ming language. However, the expressive power that makes probabilistic programming languages enticing also poses challenges to inference, so much so that specialized appro…
Amanda Liu, Gilbert Bernstein, Adam Chlipala, Jonathan Ragan-Kelley
Producing efficient array code is crucial in high-performance domains like image processing and machine learning. It requires the ability to control factors like compute intensity and locality by reordering computations into different stages and granularities with respect to wher…
Jiawen Liu, Weihao Qu, Marco Gaboardi, Deepak Garg, Jonathan R. Ullman
Data analyses are usually designed to identify some property of the population from which the data are drawn, generalizing beyond the specific data sample. For this reason, data analyses are often designed in a way that guarantees that they produce a low generalization error. Tha…
Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley
Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are not…
Justin Lubin, Jeremy Ferguson, Kevin Ye, Jacob Yim, Sarah E. Chasins
We present an enumerative program synthesis framework called component-based refactoring that can refactor "direct" style code that does not use library components into equivalent "combinator" style code that does use library components. This framework introduces a sound but inco…
Matthew Lutze, Magnus Madsen
We present associated effects, a programming language feature that enables type classes to abstract over the effects of their function signatures, allowing each type class instance to specify its concrete effects.
Associated effects significantly increase the flexibility and exp…
Konstantinos Mamouras, Alexis Le Glaunec, Wu Angela Li, Agnishom Chattopadhyay
Regular expressions are commonly used for finding and extracting matches from sequence data. Due to the inherent ambiguity of regular expressions, a disambiguation policy must be considered for the match extraction problem, in order to uniquely determine the desired match out of …
Gabriel Matute, Wode Ni, Titus Barik, Alvin Cheung, Sarah E. Chasins
Lightweight syntactic analysis tools like Semgrep and Comby leverage the tree structure of code, making them more expressive than string and regex search. Unlike traditional language frameworks (e.g., ESLint) that analyze codebases via explicit syntax tree manipulations, these to…
Benjamin Mikek, Qirun Zhang
SMT solvers are foundational tools for reasoning about constraints in practical problems both within and outside program analysis. Faster SMT solving improves the performance of practical tools and expands the set of tractable problems. Existing approaches to improving solver per…
Mark Moeller, Jules Jacobs, Olivier Savary Bélanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, Alexandra Silva
We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for buil…