Satisfiability Modulo Theory (SMT) solvers are foundational to modern systems and programming languages research, providing the foundation for tasks like symbolic execution and automated verification. Because these solvers sit on the critical path, …
Database Management Systems (DBMSs) are notoriously hard to test because you need a test oracle — a way to know if the output is correct. Prior work builds these oracles by hand, creating a never-ending cycle of manual effort. Argus breaks this cycle …
Vector Database Management Systems (VDBMSs) have become critical in LLM-integrated applications. However, their inherent complexity, including high-dimensional data structures, diverse indexing strategies, and heterogeneous implementations, makes …
Explaining with examples is an intuitive way to justify AI decisions. However, it is challenging to understand how a decision value should change relative to the examples with many features differing by large amounts. We draw from real estate …
Modern relational databases provide multiple isolation levels, yet achieving full serializability often incurs significant performance overhead. Recent research shows that, by restructuring specific query patterns, workloads can preserve …
Modern computer hardware keeps paying a performance tax for vulnerabilities discovered too late. Each generation brings dozens to hundreds of post-silicon security issues, and fixes often arrive as heavyweight patches such as microcode updates, extra …
Large language models (LLMs) and Retrieval-Augmented Generation (RAG) are increasingly integrated into software systems to realize intelligent features. However, this integration poses significant challenges due to undefined interface specifications, …
MLIR is a widely adopted compiler infrastructure that supports multi-level IRs and reusable components. Ensuring its correctness is critical, as bugs can propagate to downstream systems. MLIR provides a lowering mechanism that transforms high-level …
This is a whirlwind overview of tensor programming in machine learning compilers. We will discuss the ubiquity of linear algebra in the hardware acceleration domain and why tiling is such an important optimization for it. We then cover the various …
This paper aims to explore fundamental questions in the era when AI coding assistants like GitHub Copilot are widely adopted: what do developers truly value and criticize in AI coding assistants, and what does this reveal about their needs and …