The US visa process can be a joke. This summer, my wife and 6-year-old child planned to visit me in Blacksburg, VA. My wife got unexpected delays due to her work and study topic from more than a decade ago. Eventually, my child had to fly to the US as an unaccompanied minor. When my wife’s visa came through, it was almost time for our child to head back for his school year.

It’s sad to see the intricacies and inefficiencies in the US immigration system. Illegal immigrants get through anyway; those who follow the rules suffer.

On a brighter note, despite the challenges, we made the most of our time together. Here is a cherished photo from our trip to the Virginia Safari.

O’Hearn’s Incorrectness Logic (IL) has recently gained a lot of traction in the programming languages community. While studying it with VT faculty and students, I became captivated by IL’s power of proving the presence of bugs. Before I delve into its practical application, I aim to gain a robust understanding of its precise meaning. Below, I’ve outlined some quick notes to grasp what IL is. In the future, I may write another post to explore how IL can be utilized.

Notation 1: We represent an IL triple as [P] C [Q], where P is considered a state predicate, or equivalently, a set of states satisfying such a state predicate.

Notation 2: The expression p ->C q denotes that executing C from state p could lead to state q if C terminates.

Definition: An IL triple [P] C [Q] is valid if, for any state q in Q, there exists a corresponding state p in P, such that p ->C q.

Examples:

1. [P] C [False] is a valid IL triple for any P and C, because False represents an empty set of states.
2. [x<=1] y = x + 1 [y<=2 /\ y = x + 1] is a valid IL triple since any state in Q, e.g., (x=0, y=1), can be reached from a state in P.
3. [x<=1] y = x + 1 [y<=2] is not a valid IL triple because there exists a state in Q, (x=0, y=2), that cannot be reached from any state in P.

Hopefully, this basic understanding of IL will also serve a stepping stone for you to further investigate how this concept can be applied in various contexts.

During the summer of 2023, I have the privilege of being a visiting assistant professor at Virginia Tech. I must say that the campus is truly magnificent. However, as I attempted to capture its beauty through photography, I encountered a bit of rain.

 I am working with the Software System Research Research Group at VT and have been enjoying collaborating with their team. We are working on how to apply program analysis techniques on assembly languages to detect security issues involving illegal memory access.