Recently, I was trying to get the hang of quantum computing. I found myself in a position where I forgot most of the linear algebra stuff I’ve learned in past semesters. So again, I decide to put them down in hope that some of the knowledge here will stay in my memory a bit longer...

Border Gateway Protocol (BGP) protocol has a very simple purpose: choose the fastest and the most efficient route to deliver a message from one autonomous system (AS) to another. In layman’s term, BGP is the GPS for the internet. Many contents here are credit to Prof. Mohamed G. Gouda . In a nutshell, BGP informs each router \(R\) how to route packets to an IP prefix \(pf\) (i.e. block of IP addresses) that is used in \(AS_i\) different from \(AS_j\), where \(R\) is located:...

Since my paper on GPU benchmarking was published, every once in a while, I got emails asking me why Altis doesn’t build on their platforms. It almost always has something to do a small script which is responsible for finding CUDA dependencies. This script is invoked every single time make is executed. For some reason, the regular expression in the script sometimes breaks randomly, depending on the Linux distro, the kernel version, the host architecture, or even the CUDA version....

This is a summary over the high-level design of SAT solver covered in Prof. Dillig ’s Automated Logical Reasoning class. It’s meant to cover the basic steps towards determining whether a given boolean formula is satisfiable or not...

Because of Professor Dillig ’s class , I finally got the chance to try out Dafny , a language made by Microsoft Research , with built-in support for formal specification through preconditions , postconditions , loop invariants and loop variants . I often think, what if we write programs in a verification language, would there be much less bugs and will it make our lives much easier than sitting in front a screen for hours grinding at bugs....

In my previous post , we’ve gone over the high-level structure of blockchain and its corresponding attributes. This post is going to cover Ethereum and explore how blockchain can be used not only for money transfer but also application development....

I applied for CS Ph.D. programs this past fall and had interviews with schools from late December all the way to March. Now that the semester has ended, I decided to put down some reflections on this process. This post is not intended to be the most comprehensive CS Ph.D. application tutorial in the world, but merely a half-guide half-memoir of journey towards a PhD. Of course, you should take this post with a grain of salt, since I don’t work on admission committees, and am no where near an expert in the application process...

The first time I’ve heard the term ‘‘blockchain’’ was around 2014. Since then, its popularity has grown rapidly. However, I’ve never actually understand what blockchain is exactly, until recently. In fact, I didn’t really understand the difference between blockchain and bitcoin. For me, blockchain is clubbed with cryptocurrencies. So here is a short summary of what blockchain is and why people use blockchain...

Hoare logic forms the basis of all deductive verification. To illustrate Hoare logic, we will first consider a smaller imperative programming language IMP...

This is a summary of how to compute congruence closure. I implemented the algorithm to compute congruence closure and thought I’d never forget it. But my memory starts to get blurry just after two days. So I figured I’d put things down so I don’t have to watch the entire lecture again the next time I need it...