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...

Due to Prof. 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...

The goal here is to familiarize yourself with how programs are loaded, dynamically paged, and some of the mechanics of signal handling and memory mapping in Linux...

This is a summary on scheduler activation. To discuss about scheduler activation, we must first understand what is a thread. A thread of execution is the smallest sequence of programmed instructions that can be managed independently by a scheduler...

I was using Mathjax v2 for a while and I heard v3 perform significantly better than v2. Many great tutorials explains explains how to add Mathjax support to Jekyll websites. Some of them only cover Mathjax v2. So here is the brief summary on how to add Mathjax v3 support to your Jekyll website (Recently I’ve migrated to Hugo but adding support to Hugo is also pretty similar)...