This summer was filled with meaningful moments—both professionally and personally. On top of some exciting high points in my research at Virginia Tech, I had the joy of visiting Blacksburg with my 6-year-old. We made some incredible memories together, including a visit to the Virginia Safari Park. Here’s one of our favorite photos from the trip—such a special time for both of us.

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.