Programming Languages
This paper presents a scalable path- and context-sensitive data-dependence analysis. The key is to address the aliasing-path-explosion problem via a sparse, demand-driven, and fused approach that piggybacks the computation of pointer…
Dynamic languages like Erlang, Clojure, JavaScript, and E adopted data-race freedom by design. To enforce data-race freedom, these languages either deep copy objects during actor (thread) communication or proxy back to their owning thread.…
Fortran is the oldest high-level programming language that remains in use today and is one of the dominant languages used for compute-intensive scientific and engineering applications. However, Fortran has not kept up with the modern…
The Userfault Object (UFO) framework explores avenues of cooperating with the operating system to use memory in non-traditional ways. We implement a framework that employs the Linux kernel's userfault mechanism to fill the contents of…
Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis are divided into two groups: (1) algorithms with strong behavioral guarantees that work in limited circumstances…
Fast compilation is important when compilation occurs at runtime, such as query compilers in modern database systems and WebAssembly virtual machines in modern browsers. We present copy-and-patch, an extremely fast compilation technique…
Modularity is the fundamental aspect of modern software engineering, however many advanced modularity techniques requires prospective technologies as part of development and operation process. In this paper, we present Refinable Function,…
Many variability management techniques rely on sophisticated language extension or tools to support it. While this can provide dedicated syntax and operational mechanism but it struggling practical adaptation for the cost of adapting new…
As GPU availability has increased and programming support has matured, a wider variety of applications are being ported to these platforms. Many parallel applications contain fine-grained synchronization idioms; as such, their correct…
Programming or scripting languages used in real-world systems are seldom designed with a formal semantics in mind from the outset. Therefore, developing well-founded analysis tools for these systems requires reverse-engineering a formal…
Multicopy search structures such as log-structured merge (LSM) trees are optimized for high insert/update/delete (collectively known as upsert) performance. In such data structures, an upsert on key $k$, which adds $(k,v)$ where $v$ can be…
Gradually typed languages allow programmers to mix statically and dynamically typed code, enabling them to incrementally reap the benefits of static typing as they add type annotations to their code. However, this type migration process is…
The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols…
Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it…
In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HFL, we explain how it can be applied to program verification,…
In this paper, we present a derivative-based, functional recognizer and parser generator for visibly pushdown grammars. The generated parser accepts ambiguous grammars and produces a parse forest containing all valid parse trees for an…
A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging…
Attackers can access sensitive information of programs by exploiting the side-effects of speculatively-executed instructions using Spectre attacks. To mitigate theses attacks, popular compilers deployed a wide range of countermeasures. The…
As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes…
Smart contracts are programs that execute inside blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses, there is considerable interest in formally proving their…