File contents

TVLA - Challenges
-----------------
G. Ramalingam and M. Sagiv

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. 

TVLA 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.