167 citations · 494 across the 20 of their papers we have counts for
26 papers
An all-sky catalogue of Be transition stars from WISE and Gaia
Qi Jia, Mingjie Jian, Gang Li +2
We present an all-sky catalogue of classical Be stars undergoing transitions between quiescent B-type and active Be-star phases, based on Gaia DR3 astrometry and multi-epoch mid-in…
When Double Rounding is Correct
Brett Saiki, Bill Zorn, Cynthia Richey +1
Number libraries, which implement number formats and their arithmetic in software, are used to simulate hardware, making hardware behavior reproducible and thus verifiable and easi…
Efficient Extraction for Effectful E-Graphs
Oliver Flatt, Anjali Pal, Yihong Zhang +7
Egraphs have enabled recent advances in program optimization, synthesis, and verification, yet remain difficult to apply to effectful programs whose memory and I/O operations must…
Verification of Compiler-to-Accelerator Mappings for Machine Learning Accelerators
Akash Gaonkar, Mike He, Yi Li +8
To meet the performance needs of modern machine learning (ML) applications, ML compiler frameworks support compiler-to-accelerator mappings that offload parts of application code t…
Codetations: Intelligent, Persistent Notes and UIs for Programs and Other Documents
Edward Misback, Erik Vank, Zachary Tatlock +1
Software developers maintain extensive mental models of code they produce and its context, often relying on memory to retrieve or reconstruct design decisions, edge cases, and debu…
Target-Aware Implementation of Real Expressions
Brett Saiki, Jackson Brough, Jonas Regehr +5
New low-precision accelerators, vector instruction sets, and library functions make maximizing accuracy and performance of numerical code increasingly challenging. Two lines of wor…
Magic Markup: Maintaining Document-External Markup with an LLM
Edward Misback, Zachary Tatlock, Steven L. Tanimoto
Text documents, including programs, typically have human-readable semantic structure. Historically, programmatic access to these semantics has required explicit in-document tagging…
FPGA Technology Mapping Using Sketch-Guided Program Synthesis
Gus Henry Smith, Ben Kushigian, Vishal Canumalla +6
FPGA technology mapping is the process of implementing a hardware design expressed in high-level HDL (hardware design language) code using the low-level, architecture-specific prim…
Generate Compilers from Hardware Models!
Gus Henry Smith, Ben Kushigian, Vishal Canumalla +3
Compiler backends should be automatically generated from hardware design language (HDL) models of the hardware they target. Generating compiler components directly from HDL can pro…
Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting
Edward Misback, Caleb C. Chan, Brett Saiki +3
In recent years, researchers have proposed a number of automated tools to identify and improve floating-point rounding error in mathematical expressions. However, users struggle to…
Small Proofs from Congruence Closure
Oliver Flatt, Samuel Coward, Max Willsey +2
Satisfiability Modulo Theory (SMT) solvers and equality saturation engines must generate proof certificates from e-graph-based congruence closure procedures to enable verification…
Application-Level Validation of Accelerator Designs Using a Formal Software/Hardware Interface
Bo-Yuan Huang, Steven Lyubomirsky, Yi Li +10
Ideally, accelerator development should be as easy as software development. Several recent design languages/tools are working toward this goal, but actually testing early designs o…
Pure Tensor Program Rewriting via Access Patterns (Representation Pearl)
Gus Henry Smith, Andrew Liu, Steven Lyubomirsky +5
Tensor kernels in machine learning (ML) often correspond to pure mathematical expressions, making term rewriting an attractive strategy for optimization and mapping to specialized…
Dynamic Tensor Rematerialization
Marisa Kirisame, Steven Lyubomirsky, Altan Haan +5
Checkpointing enables the training of deep learning models under restricted memory budgets by freeing intermediate activations from memory and recomputing them on demand. Current c…
Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference
Haichen Shen, Jared Roesch, Zhi Chen +6
Modern deep neural networks increasingly make use of features such as dynamic control flow, data structures and dynamic tensor shapes. Existing deep learning systems focus on optim…
Characterizing consensus in the Heard-Of model
A. R. Balasubramanian, Igor Walukiewicz
The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We…
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang +3
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 mor…
QED at Large: A Survey of Engineering of Formally Verified Software
Talia Ringer, Karl Palmskog, Ilya Sergey +2
Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underl…
Enumerating Hardware-Software Splits with Program Rewriting
Gus Smith, Zachary Tatlock, Luis Ceze
A core problem in hardware-software codesign is in the sheer size of the design space. Without a set ISA to constrain the hardware-software interface, the design space explodes. Th…
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Chandrakana Nandi, Max Willsey, Adam Anderson +4
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…
Relay: A High-Level Compiler for Deep Learning
Jared Roesch, Steven Lyubomirsky, Marisa Kirisame +7
Frameworks for writing, compiling, and optimizing deep learning (DL) models have recently enabled progress in areas like computer vision and natural language processing. Extending…
Relay: A New IR for Machine Learning Frameworks
Jared Roesch, Steven Lyubomirsky, Logan Weber +4
Machine learning powers diverse services in industry including search, translation, recommendation systems, and security. The scale and importance of these models require that they…
A Graphical Interactive Debugger for Distributed Systems
Doug Woos, Zachary Tatlock, Michael D. Ernst +1
Designing and debugging distributed systems is notoriously difficult. The correctness of a distributed system is largely determined by its handling of failure scenarios. The sequen…
Combining Tools for Optimization and Analysis of Floating-Point Computations
Heiko Becker, Pavel Pancheckha, Eva Darulova +1
Recent renewed interest in optimizing and analyzing floating-point programs has lead to a diverse array of new tools for numerical programs. These tools are often complementary, ea…