Weekly Talk

Metamorphic Coverage

Metamorphic testing is a widely used methodology that examines an expected relation between pairs of executions to automatically find bugs, such as correctness bugs. We found that code coverage cannot accurately measure the extent to which code is …

Fortifying Software through the Lens of Neuro-Symbolic Software Analysis

Modern software is becoming increasingly difficult to secure and reason about as systems grow in complexity, adopt specialized execution environments, and increasingly incorporate AI components. Traditional software analysis provides precise …

Turning Bias into Bugs: Bandit-Guided Style Manipulation Attacks on LLM Judges

The known stylistic biases in LLM judges, such as a preference for verbosity or specific sentence structures, present an underexplored security vulnerability. In this work, we introduce BITE (BIas exploraTion and Exploitation), a black-box …

Once4All: Skeleton-Guided SMT Solver Fuzzing with LLM-Synthesized Generators

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

Argus: Automated Discovery of Test Oracles for Database Management Systems Using LLMs

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 …

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 …

Comparables XAI: Faithful Example-based AI Explanations with Counterfactual Trace Adjustments

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 …

How Should Applications Choose Optimal Isolation Levels?

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 …

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