Weekly Talk

VDBFuzz: Understanding and Detecting Crash Bugs in Vector Database Management Systems

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 …

Software-Style Hardware Testing: Information-Flow Tracking, Fuzzing, and What ML Might Add.

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 …

From Empirical Study to Runtime Mitigation: Addressing Integration Failures in LLM-Enabled Software

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, …

Finding Bugs in MLIR Compiler Infrastructure via Lowering Space Exploration

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 …

Linalg is All Your Need

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 …

"My productivity is boosted, but …" Demystifying Users Perception on AI Coding Assistants

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 …

Static bug detection in the era of LLMs

The rapid advancement of Large Language Models (LLMs) has opened new opportunities for static bug and vulnerability detection, offering complementary insights to traditional static analysis. In this talk, I will present our recent work on LLM-based …

Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle

Proof assistants are software tools for formal modeling and verification of software, hardware, design, and mathematical proofs. Due to the growing complexity and scale of formal proofs, compatibility issues frequently arise when using different …

AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents

Agents built on LLMs are increasingly deployed across diverse domains, automating complex decision-making and task execution. However, their autonomy introduces safety risks, including security vulnerabilities, legal violations, and unintended …

CrackSQL: A Hybrid SQL Dialect Translation System Powered by Large Language Models

Dialect translation plays a key role in enabling seamless interaction across heterogeneous database systems. However, translating SQL queries between different dialects (e.g., from PostgreSQL to MySQL) remains a challenging task due to syntactic …