Programming Languages
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes…
Recent program synthesis techniques help users customize CAD models(e.g., for 3D printing) by decompiling low-level triangle meshes to Constructive Solid Geometry (CSG) expressions. Without loops or functions, editing CSG can require many…
Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type system that includes functions, tensor products, additive…
Implementing graph algorithms efficiently in a rule-based language is challenging because graph pattern matching is expensive. In this paper, we present a number of linear-time implementations of graph algorithms in GP 2, an experimental…
GP 2 is a rule-based programming language based on graph transformation rules which aims to facilitate program analysis and verification. Writing efficient programs in such a language is challenging because graph matching is expensive. GP 2…
Inclusion-based (i.e., Andersen-style) points-to analysis is a fundamental static analysis problem. The seminal work of Andersen gave a worst-case cubic $O(n^3)$ time points-to analysis algorithm for C, where $n$ is proportional to the…
GP 2 is an experimental programming language based on graph transformation rules which aims to facilitate program analysis and verification. Writing efficient programs in such a language is hard because graph matching is expensive, however…
This article presents the formal syntax and semantics for a large subset of the Solidity programming language developed for the Etheruem blockchain platform based on our resent work about developing a general, extensible, and reusable…
We present a case study on using program verification tools, specifically model-checkers for C programs, to solve simple interactive fiction games from around 1980. Off-the-shelf model-checking tools are unable to handle the games in their…
Elementary Basic, published in 1982, is an introductory programming text with a novel central conceit, namely that the fictional 19th century detective Sherlock Holmes used a computer to help solve mysteries. It is also novel among similar…
MiniJava is a subset of the object-oriented programming language Java. Standard ML is the canonical representative of the ML family of functional programming languages, which includes F# and OCaml. Different program analysis and…
Deductive verification of concurrent programs under weak memory has thus far been limited to simple programs over a monolithic state space. For scalabiility, we also require modular techniques with verifiable library abstractions. This…
Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algorithm for checking CTL properties of the trees generated by…
We propose IR2Vec, a Concise and Scalable encoding infrastructure to represent programs as a distributed embedding in continuous space. This distributed embedding is obtained by combining representation learning methods with flow…
Object queries are essential in information seeking and decision making in vast areas of applications. However, a query may involve complex conditions on objects and sets, which can be arbitrarily nested and aliased. The objects and sets…
In call-by-value languages, some mutually-recursive value definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec x = x + 1) contain vicious circles and their evaluation…
We make a formal analogy between random sampling and fresh name generation. We show that quasi-Borel spaces, a model for probabilistic programming, can soundly interpret Stark's $\nu$-calculus, a calculus for name generation. Moreover, we…
This book is an introduction to program analysis that is meant to be considerably more elementary than our advanced book Principles of Program Analysis (Springer, 2005). Rather than using flow charts as the model of programs, the book…
When a software transformation or software security task needs to analyze a given program binary, the first step is often disassembly. Since many modern disassemblers have become highly accurate on many binaries, we believe reliable…
Intermediate Representations (IRs) are central to optimizing compilers as the way the program is represented may enhance or limit analyses and transformations. Suitable IRs focus on exposing the most relevant information and establish…