TVLA

Verification of Dynamic Properties with TVLA (By G. Ramalingam)

Modern software tends to be strongly dynamic, involving a set of actors that changes dynamically, and resources that are dynamically allocated and deallocated, and where no bounds are statically known for these sets. Formally, the state of such systems may be viewed as an evolving universe of entities over which the program operates. Due to its evolving character, such universes are difficult to reason about, both for programmers and for automated reasoning tools. This in turn makes automated verification for such programs both important and challenging. TVLA is a system for automatic verification of properties of such strongly dynamic systems using abstract interpretation based on three-valued logical structures. TVLA has been used to verify various safety and liveness properties of programs as well as functional correctness of programs, especially in the presence of heap-allocated data structures and concurrency.

VLA is a parametric abstract-interpretation framework. An analysis designer specifies the abstraction to be used by identifying relevant predicates (especially instrumentation predicates), which describe properties of entities in the universe. TVLA provides various primitives that make it easy to obtain the abstract semantics of statements in an automatic or semi-automatic fashion.

Many challenges and open questions remain in performing software verification using TVLA-like abstract interpretation techniques. (a) TVLA has been used to verify properties in the presence of complex heap manipulation, such as the partial correctness of quicksort implemented using lists. However, it is yet to be seen how robust the precision of these analyses are in the presence of hierarchical or nested data structures (such as lists of lists of lists). (b) Scaling TVLA so that it can handle industrial-size applications (e.g., a million lines of code) is a significant challenge. (c) We need the capability to illustrate to the user the source of potential problems in the code when verification fails. This is necessary to make verification tools user-friendly. (d) Interestingly, one of the challenges in making verification tools successful in practice is in identifying properties that one would like to have verified. E.g., a specification of the constraints on how a library should be used enables us to check that client programs that use the library satisfy these constraints. However, the lack of such formal specifications for libraries means that techniques for "mining (partial) specifications" of libraries would be valuable. On a related note, there is a need to find the right way to involve users and programmers in the verification process. A single line of formal assertion of something that's obvious to a human designer may sometimes dramatically simplify the difficulty of verification.

Some concrete approaches towards addressing the efficiency and precision challenge mentioned above are: (1) exploring techniques for doing the analysis in a modular fashion; (2) helping an analysis designer identify the right set of instrumentation predicates to use; (3) exploring the use of more adaptive and heterogeneous abstractions, where the abstraction used for different parts of the heap at different points in time can vary as needed; (4) exploring abstraction techniques other than canonic abstraction; (5) integrating TVLA-style abstraction with other abstraction mechanisms as well as other verification techniques.