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…
Satisfiability Modulo Theories (SMT) solvers are powerful tools
that answer logical and mathematical questions.
As an example, let’s say I want to know whether there exists integers
\(a, b, c\) such that \(3a^{2} -2ab -b^2c = 7\).
To ask an SMT solver, I need to write an SMT quer…
\[
\gdef\lf{\left \lfloor}
\gdef\rf{\right \rfloor}
\]
Imagine using a popular messaging app that includes a contact discovery feature to find which of your phone contacts are already using the service and to get information on how to communicate with them. While convenient, this…
Truly Anonymous Service Providers can offer users confirmed privacy, but also allow inappropriate behavior 😳
Anonymous Blocklisting permits blocking ill-behaved users without denanonymizing them. Specifically, the service provider blocks individual posts, and the benign users u…
In 2008, a groundbreaking development in the world of finance occurred: the birth of Bitcoin, the first decentralized digital currency. This innovation, introduced by blockchain technology, enables value transfer between parties without the need for traditional intermediaries lik…
In large cloud service providers such as AWS, the customer provides an attributed graph and would like to perform tasks such as recommendations (i.e., link prediction in a graph) using message-passing methods within restricted budgets.
An attributed graph consists of both the gra…
Information retrieval is a pervasive aspect of our digital life, yet the process of retrieval consistently compromises the privacy of the users (i.e., the information requesters). For example, when you access a website, you need to first retrieve the website’s IP address from a D…
Data center networks are similar to large cities:
they are at massive scale, and there exist many available roads/paths between a pair of source and destination.
To move data from one place to another, we transfer data in chunks of bytes known as packets (roughly analogous to veh…
Nobody likes waiting in line.
But some of the most frustrating experiences that I’ve ever had waiting are when I get in a super long line, I peek around to the front of the line, and I see that the server isn’t even ready to serve –they’re still setting up!
It’s terrible, and i…
As AI technology advances, more and more autonomous robots are being tasked with
navigating among people in shared environments. Such applications span academia
and industry, including sidewalk delivery robots, robotic museum
guides, and automated room service in hotels. In orde…
