The workload of state-vector quantum circuit simulation is massively parallel. Most quantum gates multiply one small matrix to many vectors, and the workload is balanced.
Challenge: the state vector is too large to be stored on one GPU, and the communication cost is very high. …
SQL is the de facto query language used to interact with databases. Since SQL is declarative, users express the intended result of their query rather than the concrete procedural steps to produce the answer. Database management systems (DBMSs) find fast execution strategies for …
In this blog post, I will begin by introducing the concept of cut sparsifier for a given graph \(G\), which has been a powerful tool in the design of graph algorithms. Following that, I will present a tight lower bound for the directed cut sparsifier of a balanced directed graph,…
Applications access their data in the memory using virtual addresses, which tell the hardware where to fetch or store a particular piece of data.
Virtual addresses are mapped to physical addresses referencing the actual memory provided by the hardware (i.e. main memory) in the …
In June, our research group released MLCEngine,
a universal LLM deployment engine powered by machine learning compilation.
MLCEngine is a single engine to enable LLM deployment across both cloud and edge devices, with full support for OpenAI API.
Performance has been one of the k…
Automated reasoning (AR) is a branch of artificial intelligence that applies various reasoning techniques to solve problems from mathematics and logic.
AR engines use clever optimizations and heuristics to solve typically intractable (e.g., NP-hard) problems.
Before a problem …
This post describes a part of our work NodeMedic-FINE, an automated tool to find arbitrary command injection and arbitrary code execution vulnerabilities in Node.js packages. While I am the sole author of this blog post, the work it describes was done in collaboration with Darion…
Randomness is a fundamental component of numerous real-world protocols. It is used everywhere, from ensuring fairness in the green card lottery to its application in clinical trials, financial audits, and various blockchain technologies.
For these protocols, randomness must satis…
In 2006, Senator Ted Stevens infamously described the Internet as a “series of tubes’‘, where “filled tubes’’ delayed his email. While Senator Stevens was ridiculed at the time for his simplistic understanding of the Internet, his characterization was not entirely wrong:
“It’s …
It is nearly inevitable that bugs will appear in a codebase during software development. To catch these bugs before they lead to real-world consequences,
the formal verification community has developed a wide variety of tools for ensuring code correctness. These tools fall
into t…
