Predictable Automatic Verification

Much of the existing work on automated verification of data structure manipulations is impacted by unpredictability, since existing works generate verification conditions in incomplete logics that must be solved using unpredictable heuristics. Therefore, it is often the case that the proof of a correct program won’t go through, forcing the engineer to perform proof engineering effort by adding lemmas and tactics, making for a frustrating verification experience. We avoid this by using local, or intrinsic definitions of data structures, rather than recursive ones, and we develop a verification philosophy that leads to predictable verification: a user provides a program and annotations that prove data structure invariants correct, and the verification problem becomes decidable. We have implemented this philosophy by verifying a range of standard data structures, including an overlay of a list and a binary search tree as seen in the Linux kernel I/O scheduler. We intend to extend our philosophy to the concurrent and distributed setting, verifying more complex systems and refining the paradigm from the engineer’s perspective.