What we learned while building JayHorn.
TODO: write about how when and where to stub library calls and how to get specification language into the game.
Our goal is to translate Java to Horn clauses that are actually solvable by off-the-shelf tools. This requires some insight into the inner workings of these solvers.
Reasoning about the heap is hard. Inferring reasonable invariants automatically requires some careful thinking about the memory model, and powerful methods (or heuristics) for generalization. For memory-safe languages (like Java, in our case), the Burstall-Bornat memory encoding has been popular for a long time. In this approach, the heap is encoded by a two-dimensional array where the first dimension describes the object that we are interested in and the second describes the field of that object that we want to access. For example, if we have a Java method like: