Advances in verification presented in TACAS’13

This special issue of the journal Software Tools for Technology Transfer (STTT) contains revised and extended versions of four papers selected out of 42 papers presented at the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13) [37]. The peer-reviewed papers collected in this special issue have been invited by the guest editors among the top papers presented at TACAS’13 based on their relevance to STTT. They all report on advances in verification that relate to domains that, in our opinion, are central to make further progress in verification.

As computers and the software that drives them become more important and more prevalent there is a growing need in ensuring that they work correctly. Verification is the field of research that aims to produce tools and techniques for proving correctness of programs and finding bugs that could hinder their performance. An active research community and much demand in industry for better and more scalable verification techniques are driving a thriving research field. In spite of much progress that was done in this field there is much scope for further research. With every success, our appetite for increasing the scope of verification increases and we try to tackle more general and bigger problems. Correctness through the life cycle of a system, scalability of verification, the challenges imposed by concurrent and distributed systems, and the importance of identification of areas where verification can be applied more efficiently are some of the domains in which interesting research is ongoing.

The selected papers cover these four domains. Our discussion of these papers is organized as follows. Section 2 discusses the verification of a system through its life cycle. Section 3 discusses compositional verification. Section 4 discusses verification of concurrent and distributed systems. Section 5 discusses the applications of model checking to recursive programs that have integer variables. Finally, Sect. 6 concludes the paper.

One of the major challenges in the software life cycle is maintenance. This includes the fixing of bugs but also the addition of features or simply restructuring of code to facilitate fixes and improvements. However, many of the techniques and tools that are developed for analysis and verification of software is targeted at new software. One can apply these techniques for existing software but the involved effort does not take advantage of previous verification efforts. Indeed, with frequent (and small) changes to the software, it is prohibitively expensive to redo the verification effort from scratch. The formal methods community is putting more efforts into the usage of its tools and techniques during the life cycle of a system.

In [11, 39] the authors introduce the concept of substitutivity, where a part of a software system replaces a different part and the task of verification is to check that all required behaviors of the previous component are still available and that no new behaviors that lead to the violation of specification are added.

This idea is extended encompass the concept of regression testing in [25]. Regression testing is well known for both software and hardware testing. A large set of tests is collected that checks many features of the design. Changes to the design are validated by running the regression and ensuring that the results match those of the previous version. Godlin and Strichman suggest that two related programs can be checked for equivalence utilizing the similarity between the two programs to facilitate the proof of equivalence. This idea is also very appealing in the absence of formal specification as the previous version of the program can be used as de-facto specification. One of the problems with this approach is that complete equivalence is too restricting. The authors of [25] consider various ways to allow for equivalence modulo some beneficial changes. In [4] the authors consider ways to improve efficiency of regression verification by distinguishing between behaviors that are impacted by the change and those that are not impacted by the change between the two versions.

A similar usage of the similarity of the program is applied in the context of existing verification efforts in [30]. Here, a subset of the assertions checked over the original program is considered and the goal of the verification task is to find scenarios according to which the original program and the new program differ regarding specific assertions. The assertion checking can be applied compositionally by considering functions or parts of the program and does not need to take into account the entire program.

Using the results of previous verification efforts has been applied also in the context of symbolic execution of programs [23]. The authors consider whitebox fuzzing [24], where symbolic executions of a program are used to drive dynamic tests for the program. In order to reuse part of the effort that went into the symbolic execution and its analysis, the authors suggest to keep summaries of the symbolic executions. It is then easier to check whether previous summaries are still applicable to the new version of the program rather than performing symbolic execution from scratch. From existing program summaries, it is easy to produce new test cases saving significant resources.

This is the topic of the paper Flexible SAT-based Framework for Incremental Bounded Upgrade Checking by Fedyukovich et al. [20], which extends the TACAS’13 conference paper [19]. They operate in the context of bounded model checking of software programs. They assume that a program that has been successfully verified in the past has been changed and needs a new verification effort. In order to apply this technique, the initial verification effort needs to be extended by further analysis. This further analysis extracts summaries of the behavior of analyzed functions. These summaries can then be used for checking the new version of the program. For functions that have not changed or changed in a way that maintains their behavior the existing summaries can be proven by considering relatively small parts of the program. It is important to note that summaries are artifacts that relate to the global correctness argument and hence abstract the full behavior of the functions. Thus, it is conceivable that even changed functions maintain the same correctness criteria. But even functions that do change can rely on summaries for the functions that they are calling and there is much hope that (if the new program is indeed correct) the new analysis effort will not have to go all the way to the root of the program. The authors report on their technique and its implementation in a tool called eVolCheck. They also included several case studies that show the benefit of applying this technique.

One of the most challenging aspects of verification is the size of the systems that are being handled. One of the approaches to tackle this problem is to suggest compositional techniques that allow to reason about parts of the system but deduce properties of the entire system. Generally stated, the idea of assume-guarantee, is to consider a part \(P_i\) of a larger system and prove that \(\langle {a_i}\rangle M\langle {g_i}\rangle \), i.e., that under the assumption \(a_i\) the part \(P_i\) guarantees the guarantee \(g_i\). Then, relationships between the assumptions of the different parts and the guarantees of other parts need to be established so that when the parts interact all assumptions hold and, as consequence, all guarantees hold as well. The advantage is that most reasoning is done at the level of the parts of the system, which are smaller and easier to handle. The interest in such techniques started very early in the history of verification. Notably, Owicki and Gries suggested a framework for compositional verification of concurrent programs [35]. Their work inspired the extension of the assume-guarantee approach to, e.g., temporal-logic reasoning [38].

One of the main obstacles to application of the compositional approach to verification is the complexity of assumptions and (local) guarantees that together are able to imply the global correctness goal. Much research has been dedicated to different approaches that try to automatically divine the different parts of the proof. For example, learning algorithms were suggested to learn general assumptions about the different parts of the system [12, 13, 36]. The idea is to have a learning algorithm create a candidate for an assumption and use failures of the proof to give the learner ideas on how to refine its candidate. A related approach replaces the learning by abstraction and abstraction refinement [8]. An abstraction of one part is used as a guarantee of this part hoping that it will be strong enough to discharge the guarantee of other parts. If this fails, the counter example is used as either a real counter example or to refine the abstraction. From a different field, Calcagno et al. perform compositional verification of heap manipulating software programs using Separation Logic [10]. Starting from Hoare triples describing the preconditions and postconditions of existing functions they use abduction to infer extra conditions on the structure of the heap that are required to discharge the postconditions. These inferred preconditions then need to be discharged by themselves by reasoning about other parts of the code.

It is in this scope that the paper Synthesis of Circular Compositional Program Proofs via Abduction by Dillig et al. [18], which extends the TACAS’13 conference paper [31], suggests a way to synthesize the parts of a compositional proof of correctness. The authors suggest several proof rules that allow for circular dependencies between the different assumptions and guarantees but are still sound in their conclusions. The general framework partitions the global proof to a sequence of subgoals that need to be discharged. A distinct advantage of their approach is that they allow for the combination of multiple approaches for the discharge of different subgoals. What’s more, the failure to prove certain subgoals can lead to their technique suggesting the partition of the subgoal to further sub-subgoals, which are then attempted using the same approach. This gives rise to an overall lazy approach to compositional verification whereby the approach starts from general goals and finds by itself the structure of the proof that will prove these goals.

Concurrent and distributed systems have always interested the verification community. However, over the past few years, two major processes have led to concurrent and distributed systems to increase considerably in prevalence and in importance. First, multi-core processors are replacing the increase in processor speed as the main tool to increase the power of processors. This arises from the physical implications of heat dissipation in processors and making increases in speed physically impossible. Second, the emergence and prevalence of communication caused an explosion in the need and supply of programs that interact and collaborate to fulfill a common goal. However, concurrent and distributed systems pose even further challenges to verification. Such programs have all the features that make verification hard (such as variables ranging over infinite domains, usage of heap, recursion) but in addition include additional features of concurrency, communication, and synchronization. For example, when trying to verify a data structure that is intended to be used in a concurrent environment one has to cope with the usual difficulties of verification. Namely, the data structure is unbounded and uses the heap to store data. Furthermore, the data itself come from infinite domains. In addition to these difficulties, in the concurrent setting, verification has to reason about a potentially unbounded number of threads accessing the data structure. Thus, the unboundedness of checking arises in three different axes. The breadth and wealth of work done on verification of such systems makes it impossible to describe here. We choose to highlight some work on linearizability that is related to the work that appears in this special issue.

The correctness criterion suggested to verify concurrent data structures is that of linearizability [27]. Some recent approaches to checking linearizability include the following. Being able to prove that a concurrent data structure is linearizable is a major challenge that called much attention to it. For example, in [3] data structures that are based on a concurrent implementation of a singly linked list are verified by maintaining a connection between the concurrent and a sequential implementation of the same data structure. In [32], the authors use refinement between the concurrent and the sequential data structures to verify linearizability without specifying explicit points where the concurrent data structure can be identified with the sequential. Vafeiadis shows how to combine rely-guarantee with separation logic to compare the linearization points of a concurrent data structure with its sequential version [41, 42]. Another attempt to remove the need to identify the linearization points is presented in [34] and replace them by verifying local invariants on the threads that imply a global invariant on the data structure.

In the paper An Integrated Specification and Verification Technique for Highly Concurrent Data Structures by Abdulla et al. [2], which extends the TACAS’13 conference paper [1], the authors consider the topic of verifying data structures that are used in a concurrent environment. They combine several approaches in order to enable automatic verification. They use a novel type of automata and apply the automata-theoretic approach to verification using them. These automata are particularly suitable for capturing the correctness criteria of such data structures. Furthermore, they use static analysis to capture the state of the heap and follow reachability between pointers on the heap. Data abstraction is used in order to handle the infiniteness of the data domain by restricting the number of times that a value appears in the data structure to one. For the unbounded number of threads, they show that considering two threads is sufficient for checking the correctness of these properties. The approach is implemented and in addition to verifying (automatically) data structures that have not been verified in the past they show that for cases that have been in the scope of previous tools the new techniques affords some acceleration of the effort involved in verification. The TACAS’13 paper [1] already inspired further work. For example, in [9] the approach is extended to more expressive properties and handles more data structures.

Over the years, the verification community dedicated much attention to programs whose variables are restricted to integer variables. Such programs appear in many domains and the removal of floating point variables has proven to be very beneficial. The approach led to many successful verification efforts. Increasing the scope of verification and allowing to verify large code bases effectively.

Software model checking has made a huge progress in the past 10 years alongside the major progress in satisfiability (SAT) and satisfiability modulo theories (SMT) solving techniques. Several tools for checking whether errors are reachable concentrate on programs that manipulate integer variables and concentrate on the control flow in such programs. For example, tools such as Impact [33] and SeaHorn [26] harness the strength of SMT solvers with the theory of integers (and linear inequalities in particular) to offer scalable solutions for reachability analysis of software (cf. [7] for a presentation of additional related tools). Such tools have also been harnessed for model-checking efforts that consider temporal-logic model checking [14‐17]. One of the important aspects of software model checking has been the combination of over- and underapproximation [5, 6] as can be seen in, e.g., [28], where it is applied to the analysis of recursive programs just like the paper included in this special issue.

In the paper Underapproximation of Procedure Summaries for Integer Programs by Ganty et al. [22], which extends the TACAS’13 conference paper [21], the authors analyze recursive programs that use integer variables. They compute underapproximations of program behavior by bounding recursion and analyzing the resulting programs using existing tools for underapproximations of non-recursive programs. They show how to generalize the results for the potentially unbounded usage of recursion and under what conditions on the recursive program the result is complete. They also present an experimental evaluation of the technique.

We have discussed some recent advances in verification and presented papers selected from those presented in TACAS 2013. These papers highlight areas of research that we believe are important for continuing success of verification. We have discussed the following topics. How to consider verification throughout the life cycle of a system and how verification techniques can be modified in order to support that. The issue of compositional verification and its relation to improving the capacity of verification. How to apply verification to concurrent and distributed systems. The importance of restricted domains for application of verification such as integer programs.