Project Description

From Averiss

Contents 1 Goal and Context 1.1 Motivations 1.2 State of the art 1.2.1 Model-checking 1.2.2 Program analysis 1.2.3 Games and modular verification 1.3 Existing related projects 2 Project description 2.1 Introduction 2.2 Program models, abstraction, and model extraction 2.3 Symbolic representation structures 2.4 Algorithmic verification techniques 2.5 Verification of open systems 2.6 Games and modular verification 2.7 Probabilistic verification 2.8 Stochastic games 2.9 Tool development and experimentations 3 Intended results and work plan 3.1 Intended results 3.2 Work plan 3.2.1 First year 3.2.2 Second year 3.2.3 Third year 4 Partners 4.1 LIAFA 4.2 LaBRI 4.3 LSV 5 Skills, Complementariness, and Collaborations 5.1 Complementariness and existing collaborations 6 Tasks and deliverables 6.1 Tasks 6.2 Participation to tasks and collaborations 6.2.1 Participation to tasks 6.2.2 Intended collaborations 6.3 Deliverables 7 Project organization and management 7.1 Working groups and project meetings 7.2 Coordination 8 Footnotes 9 References

[edit] Goal and Context

The goal of this project is to provide advanced techniques for automatic software verification, taking into account complex features of software systems written in modern and widely used programming languages (e.g., C, Java, C++, etc). Among the important features to consider, we mention for instance : data manipulation, procedure calls, parameterization, process creation, concurrency, inclusion of external code, etc.

The approach we plan to develop in order to tackle the problem is based on a tight combination of (1) abstraction techniques, applicable directly to the source code of the programs, allowing to extract automatically accurate, potentially infinite-state, automata-based models, and (2) algorithmic techniques for the (exact/approximate) analysis of these expressive models. The applicable abstractions must be automatically defined, and refined by need using the result of the analysis. The analysis techniques will be based on symbolic model-checking for infinite-state systems using finite (automata/logic-based) representations of infinite sets of system configurations.

We intend developing algorithmic verification methods for both the verification of safety properties as well as for checking termination of programs. Moreover, these verification problems will be considered for closed systems (where all components are fully defined) as well as in the case of open systems where some of their components are partially specified (e.g., for the case of programs with external code invoking).

The verification methods and techniques developed in the project will be implemented in new software verification tools, and will be experimented on challenging verification problems of real size software systems such as kernels of operating systems and web servers.

[edit] Motivations

Software systems are increasingly used in advanced industrial applications and many domains related to our modern life (e.g., telecommunication, multimedia and entertainments, transportation, commerce, health, etc.). It is widely admitted that there is a real need of rigorous and automated techniques for software analysis and verification which guarantee a high level of reliability. This need has been recognized by several major industrial software producers in all application areas. An important requirement on such methods is that they must be applicable to the source code of the software systems since it is crucial to verify the real program which will be executed and which is written in common languages (such as C, Java, C++, etc).

Model-checking is one of the most successful approaches in computer-aided verification which allows to handle automatically complex systems. This approach has been widely developed in the 80’s and 90’s, and was successfully applied in the verification of industrial size hardware systems and communication protocols. This success has encouraged research efforts investigating the application of model-checking techniques to the verification of software systems. It turns out that adapting automatic verification techniques such as model-checking to the verification of complex software systems is far from being straightforward. Software verification constitutes indeed a real scientific and technical challenge. This is due to many features of software systems which make their behaviors extremely hard to predict and analyze. Among the sources of complexity, we can mention the following ones:

• Infinite data domains : The behaviors of programs depend on input data values (parameters) ; programs manipulate local/global variables and data structures. Parameters, variables, and data structures may range over infinite domains such as reals, integers, arrays of integers, etc.

• Procedure calls : Programs contain naturally procedure (or method) calls. Therefore the control of the program depends on the (dynamic) context stack. The size of this stack can be arbitrarily large (or parametric) depending on the number of nested (potentially recursive) calls. Moreover, when program variables range over infinite domains, or refer to shared (global) data structures, the structure of the context stack may become very complex.
  Another source of complexity is the use of higher-order functions (which is allowed for instance in functional programming languages). In this case the context stack has a nested structure since each context at some level may itself contain a context stack of a lower level, and so on.

• Process creation and concurrency : Programs may create dynamically parallel processes (or threads) which can communicate (exchange information) and synchronize (wait for each other at some point)^[1]. The number of such threads can become arbitrarily large and may vary during the execution. Again, dealing with multithreaded programs is even more difficult if threads can synchronize through shared (unbounded domain) variables and data structures.

• Invoking external code : Software systems are in general designed in a compositional way, reusing existing pieces of code and calling imported methods from external modules and libraries which may be of different origins. The source code of the methods in the invoked external modules may be inaccessible, and only high level specifications of them may be available.

In the last few years, an important effort has been devoted to the extension of the model-checking approach to software verification. Taking into account each of the features mentioned above is actually by itself a hard task and requires the conception of new models and related verification algorithms. The task becomes even harder when several of such features must be taken into account. This complication is nevertheless unavoidable if we want to handle real-life programs.

Regarding the features listed above, one major difficulty to face, raised by the three first items in the list, is that the needed models are in general infinite-state (i.e., they may have an infinite set of reachable configurations) whereas classical model-checking algorithms were designed for dealing with (large but) finite-state models. The last item in the list raises the problem of open system verification, i.e., verifying a system (or a part of it), taking into account all its possible contexts (i.e., environments corresponding to external components, users, etc). In such a case, techniques for modular or compositional verification are needed. The issue of infinite-state verification and modular verification are actually orthogonal, but they become of course harder to tackle if considered together, which is in fact needed in order to reason about complex systems.

One way to approach the problem is to use abstraction techniques. The goal is to reduce the verification of (infinite-state) software systems to verification of finite-state models (and therefore applying existing model-checkers). Works in this line develop automatic abstraction techniques (such as the so-called predicate abstraction [1]) which allow to produce abstract boolean programs. In this approach, the main problem is in fact to find automatically an accurate enough abstraction which allows to establish the desired property. Indeed, when a property is falsified and a counterexample is found, it could be due to the inaccuracy of the abstraction. In that case, abstraction refinement techniques based on counterexample analysis are applied to derive automatically a more accurate abstraction. The resulting approach called CEGAR (CounterExample Guided Abstraction Refinement)[2, 3] has been implemented in different tools such as MAGIC [4], BLAST [5, 6, 7], and SLAM [8]. These tools have been used successfully in the analysis of huge programs such as drivers, robot controllers, etc. However, programs considered so far using these tools exhibit relatively simple features. For instance these tools can hardly deal with programs with features such as dynamic creation of concurrent threads, data dependency and handling of data structures.

Another line of research attempts to develop new model-checking algorithms for richer infinite-state models based on extended automata, i.e., finite control state machines supplied with variables of data structures such as counters, stacks, queues, etc . Works in this line are based on symbolic reachability techniques using (1) representation structures for the manipulation of potentially infinite sets of configurations, and (2) procedures for computing representations of the sets of forward/backward reachable configurations. Representation structures can be either automata-based or logic-based, and reachability analysis procedures use powerful fixpoint acceleration techniques to help or enforce termination. This approach has been applied for several classes of infinite-state models. In particular, it has been applied for models which are relevant for program verification, e.g., pushdown systems [9, 10, 11, 12] , counter automata [13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23], Process Rewrite Systems (which subsume Petri nets and pushdown systems) [24, 25, 26, 27], dynamic networks of pushdown systems [28], dynamic memory and pointer systems [29, 30, 31]. However, these advanced model-checking algorithms still have to be enhanced in order to deal with wider classes of models and programs. For instance, the treatment of synchronization between concurrent processes, as well as the classes of memory structures which can be handled, are still relatively restricted. Moreover, these works apply to abstract (infinite-state) models and not to program code. An automatic translation from source code to the considered models is needed in order to exploit these powerful model-checking techniques.

Therefore, our conviction is that, in order to develop a “general” automatic verification approach for complex software systems, we need (1) to design new model-checking algorithms applicable to expressive infinite-state program models, and (2) to embed these algorithms in a CEGAR-loop based framework allowing to extract automatically abstract models and to analyze them using these new infinite-state model-checking techniques. The project aims at developing such an approach and at implementing it in efficient tools.

The objective of the project is to develop advanced verification techniques allowing to enhance the capabilities of the software verification tools and to extend their applicability to wider classes of programs. Our aim is indeed to provide algorithmic verification methods allowing to handle important classes of programs which are beyond the scope of the existing verification methods and tools. The approach we will adopt is based on a tight combination of (1) abstraction techniques allowing to extract automatically from the source code of the programs abstract models which are accurate enough for the verification purpose with (2) symbolic infinite-state model checking algorithms which are applicable to these models. Therefore, the intended work in the project concerns more precisely :

• The definition of expressive program models based on extensions of automata capturing different important aspects in program behaviors. We will consider models allowing to handle various classes of programs with complex control structures and with manipulation of data over infinite value domains. In particular programs with procedure calls, process creation, interruptions and exception handling, local/global variables, value passing, communication and synchronization through shared variables and data structures.

• The development of algorithmic verification techniques for the models mentioned above (which are in general infinite-state). We will consider automated verification techniques for checking safety properties (e.g., invariance properties) as well as for checking termination of programs. Moreover, we intend to consider these verification problem for both closed systems and open systems (interacting with an external environment).

• The development of abstraction and automatic model extraction techniques, including counterexample-guided abstraction refinement principles, targeting the considered models.

• Construction of prototype tools implementing these techniques and their experimentation on significant examples of software systems. The challenge is to be able to apply our techniques to (significant parts of) software systems such as kernels of operating systems (like Linux, NetBSD, FreeBSD), micro-kernels such as L4, or Web servers such as Apache.

[edit] State of the art

We give hereafter a broad view of the related approaches and works to our project. We mainly present and compare the works in the communities traditionally known as ”model-checking” and ”program analysis” communities and which are now converging to the problem of automatic software verification. We also mention the important research activity around the problem of modular verification (and verification of open systems) which is closely related to problems on 2-players games.

[edit] Model-checking

The model checking community has devoted a lot of effort in the past to the verification of mainly hardware systems and telecommunication protocols. Its original approach is based on finite-state models which are analyzed for a wide range of properties using efficient state-space exploration/representation algorithms. Recent research in this community tends to extend the applicability of model-checking techniques to software verification. They follow mainly two complementary lines of research : Abstraction + finite-state model-checking : which consists of using powerful abstraction techniques including automatic refinement schemas in order to derive from the program codes abstract finite-state models which can be analyzed by standard model-checkers. Several teams are working in the so-called CEGAR (CounterExample Guided Abstraction Refinement) approach [2, 3] including SLAM [8] at Microsoft research, BLAST [5, 6, 7] at the university of Berkeley (and now at EPFL), and MAGIC [4] at Carnegie Mellon University. Participants to this project have participated to the development of some of these new generation verification tools : Tayssir Touili (from LIAFA) is involved in the development of MAGIC [32] and its extension to concurrent programs with procedure calls, and Grégoire Sutre (from LaBRI) was a member of the BLAST team and contributed to the development of the so-called lazy abstraction techniques [33, 34]. Infinite-state model checking : which consists of extending the capabilities of model-checkers in order to deal with more expressive (infinite-state) models which allow to capture various features in software systems related to both complex control and data manipulation aspects. Members of this project have extensively contributed to this approach by considering, e.g., recursive procedure calls using pushdown systems [11, 35], multithreading and process creation using process rewrite systems and networks of pushdown systems [24, 25, 26, 27, 28, 36, 37], queuing mechanisms and asynchronous communication using (lossy) fifo-channel systems, counting and manipulation of integer/real variables using counter systems and Petri nets [38], dynamic memory and pointer manipulation using extended word/tree automata [39, 40], etc. Tools implementing infinite-state model checking techniques are already available such as BABYLON (Brussels), LASH (Liège), FAST (LSV and LaBRI), Moped (Stuttgart), TReX (LIAFA), etc.

While the first line of research considers basically finite-state model-checking (except that some of the tools start recently to handle pushdown systems as models of sequential programs), the second line of research considers the model-checking problem at the model level and not at the source code level.

[edit] Program analysis

The community of program static analysis has traditionnally concentrated on software analysis by means of various abstract analysis techniques. These techniques are applied directly to program codes and are in general quite efficient, but they are tailored to particular properties and use approximate analysis algorithms (using upper approximations of the state space). Techniques have been developed for instance to deal with programs with integer/real variables [41, 42, 43, 44], programs manipulating pointers [45, 46, 47, 48, 49, 50, 51, 52], etc.

The two communities of model-checking and program static analysis are now converging to the same problem of program verification. Since the last few years, there are more and more collaborations between researchers in the two communities leading to combinations of their approaches and techniques allowing to tackle more complex verification problems on wider classes of programs. Researchers in our project, e.g., Tayssir Touili and Ahmed Bouajjani from LIAFA, have collaborations with researchers from the community of program static analysis [28, 32, 53]. The two communities share in fact a common background. Their approaches are both based on computing fixpoints corresponding to abstract representations of the reachable configurations in a system. In model-checking, an abstract model is first derived, and then a precise analysis of this model is performed. In the case of static analysis (based on abstract interpretation [54]), the analysed object is close to the original system but the analysis techniques use abstract (approximate) computations of the set of reachable configurations which is in general infinite.

Work on abstract analysis of programs is close in spirit to the work on symbolic infinite-state verification which is developed in the community of model-checking. Indeed, both of the communities use expressive representation structures for infinite sets of configurations, based on automata [19, 20, 21, 23, 24, 25, 26, 27, 28, 29, 36, 37, 55, 56, 57, 58, 59, 60, 61, 62], logics [30, 31], or other related data-structures (such as (parametrized) DBMs [18], octagons and polyhedra [41, 42, 43, 44], etc), and use acceleration techniques (exact or approximate), such as meta-transition computations [63] or widening techniques [41, 58, 60, 62, 64], in order to help or enforce the termination of the reachability analysis.

In our project, we will investigate algorithmic verification techniques which combines approaches from the three communities mentioned above, namely abstract model extraction with (counterexample guided) refinement principles, infinite-state model checking, and symbolic abstract analysis.

[edit] Games and modular verification

The verification problem of open systems can be reduced to the problem of solving 2-players games on the state graph of the considered systems. Indeed, a correct computation of an open system (w.r.t. some given property) can be seen as a game against the (uncontrollable) environment : for all possible actions that the environment may perform at each step, the system must be able to choose an action to perform such that the resulting infinite computation (composed by actions from the environment and the system) satisfies the given property. In games terminology, this means that the system has a winning strategy against the environment. There exist a lot of activity around the problem of solving various kinds of games and the application of these games in modular verification. However, most of these work consider the case of finite-state program models. There are also works on some infinite-state models such as, mainly, pushdown systems and timed automata, and also few works on lossy channel systems and some subclasses of Petri nets. Still, works on modular verification for complex program models (such as for multithreaded programs, programs with data manipulation, etc) are lacking. Therefore, we intend in our project to develop efficient algorithmic methods and techniques for solving games over infinite-state program models and to apply these techniques to modular verification of programs with complex control and data manipulation.

[edit] Existing related projects

The teams of this project are involved in the following national projects which are related to the topic of this project.

• DYNAMO (ACI sécurité). July 2003-July 2006. Partners : VERIMAG (Sergio Yovine - coordinator), LIAFA (Peter Habermehl). This project concentrates on the verification of programs with pointers using automata based techniques such as regular model checking or counter automata. In that project, pointer manipulation is considered in the case of iterative sequential programs. Pointer manipulation is not considered in the presence of other features such as procedure calls, multi-threading, data manipulation, etc. The verification is considered at the level of abstract models (and not program code).

• PERSEE (ACI sécurité). July 2003 - July 2006. Partners : LSV (Philippe Schnoebelen - coordinator), LaBRI (Grégoire Sutre), LIAFA (Ahmed Bouajjani). This project considers the verification problem of heterogeneous communicating extended automata (timed automata with counters and FIFO channels) with application to the verification of telecommunication protocols. While some of the techniques developed in this project (such as symbolic reachability using automata-based representations) are related to the ones we intend to use in AVERISS, they are still not adapted to the classes of models we are aiming to consider now.

• AVERILES (RNTL). January 2006-December 2008. Partners : LIAFA (Peter Habermehl - coordinator), CRIL technology (Bertrand Tavernier), EDF ( ), LSV (Philippe Schnoebelen), VERIMAG (Radu Iosif). Verification of industrial-size programs with pointer manipulations. Aspects such as procedure calls, data manipulation are not considered, and multi-threading is limited (fixed number of threads with simple communication schemas). The main focus in that project is made on intrinsic errors detection (such as risk of memory leak). In AVERISS, we intend to develop a more general framework for software verification.

In the international context, there exist several projects on software verification. This is indeed a very active and competitive research area. Software model checkers using the CEGAR approach are developed in different academic and industrial laboratories, e.g., the tool BLAST (Berkeley University and Lausanne), MAGIC (Carnegie Mellon University), SLAM/ZING (Microsoft Research), and jMoped (University of Stuttgart). As mentioned above, the current versions of these tools are based on finite-state model checkers (or for some of them, they use some analysis using pushdown reachability to deal with procedure calls). Therefore, their handling of complex features such as multi-threading (with dynamic creation of processes), data manipulation, pointers, etc, is still very limited and under investigation. We think that our project can provide verification tools with more capabilities than the existing ones by enhancing their CEGAR-loop technology using our advanced infinite-state model-checking techniques for more accurate and expressive program models.

[edit] Project description

[edit] Introduction

To achieve the objectives of the project mentioned above, the work in our project will follow several closely connected research directions concerning both theoretical and practical aspects.

Program models : We intend developing new program models and studying their expressiveness and decidability properties. We will define models based on extended automata (i.e., automata supplied with variables and data structures) allowing to reason about features related to complex control (procedure calls, dynamic process creation, concurrency, interruption and exception handling, etc), data dependency (manipulation of local/global variables and parameters ranging over possibly infinite data domains, communication through shared variables and data structures, etc). We also intend to develop automatic techniques allowing to build systematically such (abstract) models from the source code of programs.

Automatic verification techniques : We intend to develop verification algorithms for these (a priori infinite-state) models. We are first interested in determining significant classes of models for which verification problems are decidable. For these classes, we will study the complexity of the verification problems and provide efficient algorithms solving them. Moreover, we intend to develop generic verification techniques which can be applied efficiently in practice to classes of models for which the verification problem is in general undecidable. These techniques will be based on adequate formalisms for symbolic representation and manipulation of infinite sets of program configurations, and on powerful techniques for automatic generation of the sets of configurations satisfying a given property, e.g., the set of all reachable configurations from a given set of initial configurations, or the set of all configuration from which the execution of the program will eventually terminate. Of course these techniques cannot be complete. The best we can hope for is that either they give an exact answer when they terminate, or they always terminate but give only approximate results. However, even if the result is approximate, it can be nevertheless accurate enough for the verification purpose. So, our aim is to provide techniques for which accuracy can be adapted to a verification objective, and which have completeness properties for significant classes of models.

Verification of open systems : We will consider the program verification problem in several contexts. The basic case is when all the components of a system are fully specified and it has no interaction with any external environment (or if this is the case, the environment is also specified and considered as part of the system). Another important verification context consist in considering open systems such as systems which must interact with an external environment (e.g., the arrival of requests from users), or systems invoking external modules and therefore some of their components are not explicitly defined. For that case, we need verification techniques which can be applied to parts of the system independently from the other missing parts. Therefore, we will address the issue of modular verification for various infinite-state program models and develop for that purpose techniques based on solving games (between two players) on these complex models.

In the context of open system verification, probabilistic infinite-state models can also be very relevant for instance to reason about uncertainties in the expected behaviors of the environment (actions of external code, arrivals of user requests, etc). Verification techniques for these models will therefore be studied.

We describe hereafter in more detail the research direction mentioned above. We identify the problems and challenges we will address, and present the approaches we intend to adopt to tackle these problems.

[edit] Program models, abstraction, and model extraction

Given (the source code of) a program, we need automatic techniques able to extract abstract models on which verification techniques (such as symbolic reachability analysis and model-checking algorithms) can be applied. For that we need first to define faithful formal models for interesting and representative classes of programs, and then to study abstraction techniques allowing to build systematically such models from the source code of a program, and to refine the level of abstraction by need depending on the verification purpose.

The challenge here is to be able to find the good trade-off between expressiveness and tractability. We would like indeed to, given a class of programs and a class of properties, provide abstract models which (1) allow to define a complete analysis methodology, and (2) for which there are efficient algorithmic analysis techniques.

We intend to define such models based on various classes of automata extended with variables and registers, and data structures such as stacks, queues, or arrays. Closely related models can be defined in terms of (word/tree) rewrite systems and can be sometimes more natural as models for complex programs.

We have already done in the recent few years works in this direction. We have for instance studied various kind of automata-based or rewrite systems-based models for programs with procedures, dynamic creation of processes, programs with dynamic linked lists, etc.

However, these works still have many limitations. For instance, these work do not consider programs with parameters/variables ranging over unbounded data domains (such as integers), they do not consider handling references and memory allocation/desallocation in presence of procedure calls, and when they consider parallel processes, communication schemas between these processes are quite restricted. The challenge here is to overcome these limitations in order to be able to deal with more realistic verification problems. Another challenge is to be able to define algorithmic techniques allowing to build automatically these models from the given program and property. For this, we intend to extend the concept of predicate abstraction and the related techniques in order to be able to generate not a finite-state model, but more complex models which are in general infinite-state extended automata (such as counter automata, extension of pushdown systems and Petri nets, etc).

[edit] Symbolic representation structures

Verification algorithms of infinite state systems need usually formalisms and data structures for the finite representation and the manipulation of infinite sets of configurations (in order to compute, e.g., the set of reachable configurations, or more generally, the set of configurations which satisfy some given property). Typical requirements on the representation formalism are (1) closure under boolean operation or at least union and intersection), and (2) decidability of the emptiness and inclusion problems.

We will investigate adequate symbolic representations that offer the best possible trade-off between accuracy and tractability, i.e., (1) that are precise enough to represent sets of complex configurations of programs which appear in the analysis, and (2) for which it is possible to perform efficiently all needed operations for the analysis. We will consider representation formalisms based on automata as well as formalisms based on logics (e.g., fragments of arithmetics, logics on finite/infinite structures such as trees or more general families of graphs).

Automata-based representations can be used for reasoning about a wide class of infinite-state systems. This has been shown by many works providing algorithmic verification techniques for, e.g., pushdown systems, fifo-channel systems, counter systems, parameterized networks of identical processes, process rewrite systems and dynamic networks of pushdown systems, programs with dynamic 1-successor linked structures, etc. In particular, regular model checking, a generic automata-based modeling and verification framework of infinite-state systems has been introduced and extensively studied. In this framework, configurations are encoded as words (or trees), sets of configurations are represented by means of finite-state automata, and transitions (program statements) are defined using finite-state transducers.

Logic-based formalisms are quite powerful and can also be used in reasoning about a wide range of systems. In fact, it is well known that there are tight relations between automata and logics. However, using logic-based formalism may have some advantages, mainly because it is often more natural to use logic as a specification formalism than automata which are somehow a formalism of a lower abstraction level. Of course automatic translations from formulas to automata can be useful for algorithmic reasons. Indeed, in many cases, efficient decision procedures and verification algorithms for logic based formalisms use translations and reductions to decidable problems on automata. Logics are particularly convenient for reasoning about complex structures (such as trees and some other families of graphs), and in particular to reason about the heap configurations of program with dynamic memory and pointer manipulations.

We intend in this project to define expressive symbolic representations formalisms of sets of program configurations based on automata and/or logics, and to study their fundamental properties (closure and decidability) and develop efficient algorithms for their manipulation. The main challenges are (1) to be able to capture relevant aspects in the considered classes of programs, and in particular the fact that we need to handle control aspects together with data aspects (procedure calls with parameters and local/global variables over unbounded data and memory references domains), and (2) to come with scalable techniques which allow to deal with real size systems.

For the first point, we intend in particular extending the framework of regular model checking in order to deal with (1) richer classes of configuration sets than the class of regular sets, and (2) more general structures than words and trees. We will also investigate logic based formalisms allowing such generalizations. Combinations between the two kinds of formalisms will also be investigated (for instance automata with constraints).

As for scalability, we intend to study carefully the technology behind automata manipulation and come with more efficient data structures and algorithms for expensive (an heavily used) operations (such as determinization and projection). We will also investigate efficient decision procedures for relevant logics (by exploring efficient translations to automata or using efficient constraint solving techniques).

[edit] Algorithmic verification techniques

A important effort in our project will be devoted to the definition of new algorithmic techniques for the analysis and the verification of complex program models. We will investigate the decidability and the complexity of the verification problem for different classes of program models and properties. Properties of special interest in the context of program verification are invariance properties and termination. On one hand, we will identify significant classes of program models for which the verification problem is decidable and tractable. On the other hand, we will design generic algorithmic verification techniques allowing to tackle in practice a wide range of program models.

Reachability analysis is a fundamental building block of verification algorithms. Computing immediate successors and predecessors allows to reason about strongest post-conditions (post images) and weakest pre-conditions (¬pre¬ images). Using adequate symbolic representation formalisms (with the required decidability and closure properties mentioned in the previous section), this allows for instance to check automatically that a given property is an invariant.

A more challenging problem is to compute the set of all forward or backward reachable configurations. Model-checking algorithms use typically backward reachability analysis, but forward reachability analysis can be more efficient in some cases. Moreover, computing the set of forward reachable configurations provides an invariant of the program (actually the strongest invariant set including the initial configurations).

The main difficulties to face when addressing the problem of computing reachability sets are (1) non termination in general of this computation, and (2) the size explosion of the representation structures. To tackle these problems, several approaches can be adopted. Fixpoint acceleration techniques can be used in order to help termination. Examples of acceleration techniques are those based on the computation of the (exact) effect of meta-transitions which typically correspond to the iteration (an arbitrary number of times) of some (specific classes of) transitions or control loops in the model. Other techniques are based on abstract successor computations using for instance widening operations or mappings to abstract domains. These techniques allow to force termination and to compute upper approximations of the reachability set.

We will develop such generic techniques based on either automata or logic based formalisms. We are particularly interested in approaches where the accuracy of the abstract reachability analysis can be refined by need. In this context, we will consider in particular the framework of abstract regular model checking introduced recently as a generic technique for checking safety properties [65]. This technique combines the automata-based approach for symbolic reachability analysis with abstraction techniques on automata. The principle is roughly the following : We use families of refinable abstractions on automata allowing to compute upper approximations of the reachability set. Given an abstraction, if during the reachability analysis the property is violated, the obtained counterexample is automatically analysed. If it is spurious (i.e., it does not correspond to a concrete trace in the real system), the abstraction relation is automatically refined in order to remove this conterexample. This technique has been shown quite efficient (in most of the cases, it is more efficient than the other existing techniques) and has been applied to many classes of infinite-state systems. In particular, it has been successfully experimented for the analysis of programs manipulating dynamic linked structures [66, 67].

The challenge here is to broaden the scope of applicability and the scalability of this approach. We will investigate (1) new abstraction schemas with associated refinement techniques which can be applied for an efficient analysis of various programs models, and (2) the extension of its principle to larger classes of automata allowing to handle sets of more complex program configurations, in particular, configurations including informations about the control and the data manipulated by the program.

[edit] Verification of open systems

Our project will devote a particular effort to develop verification techniques which are applicable in a modular way to pieces of code (in some of the modules) of a system, assuming that the rest of the code (in the other modules) is not given and its behaviors is not controllable (i.e., the external code can perform any action allowed through some given interface).

[edit] Games and modular verification

The approach to tackle the modular verification problem is to reduce it to a problem of solving a 2-players game on the state/transition graph of the system. Therefore, we intend to investigate the problem of solving games for various classes of program models. We have already obtained various results on games for pushdown systems [68], (and more recently for higher-order pushdown systems). We have also investigated the case of Petri nets in [69]. The research on games for infinite-state systems is however still limited and very little is known beyond the results mentioned above (except concerning timed automata). One of the challenges of our project is to extend our investigations on games for infinite-state systems to more general classes of program models. We will consider with a particular interest the case of multithreaded programs (with procedure calls and parallel process creation), and the case of programs with procedure calls and data/reference manipulation. As our work in [69] shows, such an extension is not easy (even reachability game problems are undecidable for very natural models of parallel programs such as Petri nets). We will investigate significant classes of models with decidable and tractable game problems, and we will also investigate the development of generic algorithmic techniques for solving games based on under/upper approximate computations of the winning/loosing states. Such generic techniques will be extensions of the generic techniques developed for the case of closed system verification.

[edit] Probabilistic verification

Probabilistic models can also be relevant for reasoning about open systems since they allow to model uncertainties related to the uncontrollable behaviors or actions of some external modules or users, etc. As for games, the research on probabilistic model-checking of infinite-state systems has not been addressed, except in very few recent works concerning again the case of pushdown systems (and also for lossy channel systems), see e.g., [70]. The challenge here is to investigate the probabilistic model checking problem for other classes of models allowing to deal for instance with multithreaded programs and with programs with data/reference manipulation. An interesting and quite challenging development we intend is to extend the generic framework of regular model checking to the probabilistic case.

[edit] Stochastic games

The combination of games and probabilities leads to the more general problem of solving stochastic games.Stochastic games, introduced by Shapley [71] in 1953, were traditionally used to model economical interactions [72]. However, in early 90 problems related to the verification of finite-state probabilistic systems began to attract attention in computer science and such problems can be formulated directly as stochastic games albeit with the winning criteria that are very different from the ones known from economics.

The reachability condition is the simplest condition pertinent for program verification and finite state perfect information stochastic reachability games were examined in 1992 [73]. More general winning conditions motivated by program verification were also examined at the same time but in the simpler framework of one-person stochastic games (Markov Decision Processes) [74].

We have now a rather good understanding of stochastic games related to the verification of finite state systems : there exist efficient algorithms for the verification of one-player systems [74, 75] and it is known that for two-player games both players can restrict themselves to simple deterministic positional strategies [76]. Even the most general finite state stochastic games when both players can choose their moves in parallel (partial information games) were successfully examined [77].

[edit] Tool development and experimentations

We will also devote an important effort in the implementation and the experimentation of the methods and techniques developed in the project. The symbolic analysis techniques for the infinite-state programs models will be implemented in our tools TReX and FAST. For that, new libraries of (automata/logic-based) symbolic representations must be developed. Moreover, we will embed the symbolic analysis techniques in a CEGAR-based environment allowing to build abstract models from the source code of the programs, and to refine these abstractions by need using the result of the symbolic analysis. Finally, we will apply our tools on real-size software systems. We will target challenging verification problems concerning (micro-)kernels of operating systems and web servers.

[edit] Intended results and work plan

[edit] Intended results

The work in our project aims at developing both the theoretical background and the technology which are needed for the new generation software verification tools based on combining abstraction techniques and automatic analysis and verification algorithms. We intend to improve significantly the state of the art by providing new techniques allowing to deal with programs out of scoop of the existing methods and tools. The strength of our approach is to use powerful infinite-state model-checking algorithms applicable to expressive program models instead of the standard modelchecking algorithms for finite-state models. Indeed, being able to automatize the verification for more expressive models allows to deal with less abstract and therefore more faithful program models, whereas methods based on weaker models (such as finitestate models) may fail because of the difficulty to find (systematically and efficiently) an accurate enough model.

We intend to provide by the end of the project new algorithms and methods for software verification as well as tools implementing them which can be applied to programs with significant size and complexity.

[edit] Work plan

We will consider during the project several important classes of programs, and in particular programs with the following features : multithreading (concurrency and dynamic creation of processes), data manipulation (programs with integer/real variables), value and reference passing (programs with parameters and variables ranging over the domain of integers, or the domain of memory addresses), modularity and interaction with an external environment (programs invoking external code, or managing user requests).

We plan to consider gradually the following axes of complexity : (1) the control axis : sequential programs with procedure calls, multi-threaded programs with a static number of concurrent processes, and then multi-threaded programs with dynamic creation of processes, the data axis : boolean (finite) data, numerical data (integers/reals), and references (memory addresses, pointers), and (3) the structure axis : closed systems, and then open systems.

The intended work progress and results during the project are as follows :

[edit] First year

• Formal models for sequential/multithreaded programs (procedure calls/process creation) with data/reference manipulation (data over unbounded domains, and pointers)
• Analysis for sequential programs and numerical (integer/real) data domains (both closed and open case),
• Analysis of boolean multithreaded programs
• Modular/probabilistic analysis of sequential boolean programs

[edit] Second year

• Abstraction and model extraction for C programs (targeting models defined the first year),
• Analysis of multithreaded programs with reference manipulation (without pointer arithmetic and numerical data)
• Analysis of sequential programs with numerical data domains and reference manipulation (with pointer arithmetic)
• Modular/probabilistic analysis of multithreaded boolean programs
• Modular and probabilistic analysis of sequential boolean programs

[edit] Third year

• Abstraction refinement techniques based on symbolic counterexamples (execution traces)
• Analysis of sequential/multithreaded programs with numerical data and reference manipulation
• Modular analysis of sequential/multithreaded programs with numerical data
• Modular and probabilistic analysis of sequential/multithreaded programs

[edit] Partners

[edit] LIAFA

LIAFA is a joint laboratory of the University of Paris 7 and the CNRS. It is one of the main laboratories in theoretical computer science in France, and has among its members worldwide experts in several research areas such as algorithmics, combinatorics, automata and language theory, formal modeling and verification of systems, dynamic and hybrid systems, etc.

The team “Modeling and Verification” (MV) of the LIAFA laboratory which is involved in the present project is composed of 4 professors, and over 15 researchers and PhD students, under the responsability of Prof. Ahmed Bouajjani. The team has a strong expertise and a long record of contributions in the area of model checking and algorithmic methods for verification of complex systems, especially for concurrent/distributed systems, timed/hybrid systems, and infinite-state systems, with applications in the domains of telecommunication protocols and software systems. In particular, the team is specialized in automata-based techniques for infinite-state model checking (regular model checking) and its application in program analysis.

The team MV of LIAFA has a long experience in collaboration projects, and especially in European projects. In particular, Ahmed Bouajjani was the coordinator of the FET project ADVANCE (October 2000, January 2004). The team maintain active international collaboration links with several leading research groups and researchers in the domains of computer-aided verification and program analysis, e.g., Stuttgart university (Javier Esparza), Uppsala university (Parosh Abdulla and Bengt Jonson), Carnegie Mellon University (Edmund Clarke), University of Wisconsin at Madison (Thomas Reps), University of Tel-Aviv (Shmuel Sagiv and Alexander Rabinovich), University of Liège (Pierre Wolper and Bernard Boigelot), University of Muenster (Markus Mueller-Olm), etc.

[edit] LaBRI

The Bordeaux Research Laboratory in Computer Science (LaBRI) is composed of 5 main research teams covering various fields of computer science. This ARA proposal involves the Modeling, Verifying and Testing computerized systems team (MVTsi) lead by Igor Walukiewicz.

The MVTsi team’s research activities aim at developing formal methods for complex and critical systems, with a focus on the following areas :

1. Modeling : design and enhancement of modeling formalisms (in particular the AltaRica language) for the description of complex systems and of their expected properties, with a particular emphasis on infinite continuous aspects (real-time, hybrid), on infinite discrete aspects (counters, stacks), and on stochastic aspects.
2. Analysis : design and implementation of analysis techniques for these models : symbolic verification, automatic abstraction and refinement, test case generation, controler synthesis, validation of biological models.
3. Case studies : practical evaluation of both the modeling formalisms and the analysis tools that have been developed, by experimentation on real examples (provided by industrial partners).

In this team, E. Fleury, J. Leroux, G. Sutre, A. Vincent and I. Walukiewicz are working in research areas close to this ANR proposal. Recent work include contributions on automata-based symbolic representations for integer variables, on formals methods for verifying infinite state systems such as hybrid systems, counter automata and pushdown processes, abstraction refinement for C programs, and tools applying these researches.

[edit] LSV

LSV is a joint laboratory of CNRS and ENS de Cachan created in 1996. The laboratory is one of the main laboratories in France in the domain of verification. It has around 19 permanent researchers and the same number of students and non-permanent researchers. The research activities of LSV are organized around two main axes : security, and embedded systems. In the second axis, the teal INFINI coordinated by Philippe Schnoebelen and Alain Finkel develop a research activity around symbolic verification of infinite-state models. In particular, the team developed novel techniques based on fixpoint accelerations for efficient reachability analysis of complex models, in particular for counter systems. This research is supported by national and international collaboration projects (ACI sécurité and ReX FP6 ARTIST2)

[edit] Skills, Complementariness, and Collaborations

The persons involved in this project are in an excellent position to realise the goals of the project. We first give the specific skills of the different partners, and then we describe how do we intend to collaborate.

[edit] Complementariness and existing collaborations

Complementariness : LaBRI and LIAFA have a strong experience on CEGAR techniques (Tayssir Touili is involved in the MAGIC tool and Grégoire Sutre is involved in the BLAST tool).

The three partners in the project are experts in automata-based symbolic analysis techniques : LIAFA and LSV have developed symbolic techniques that are applicable to the analysis of programs with procedure calls, multithreading, and pointer manipulation. The LIAFA has developed techniques for the analysis of counter systems based on particular representation structures for arithmetical constraints based on (parametric) difference bound matrices. The LSV and the LaBRI teams have developed an alternative approach for the analysis of counter systems based on automata representations of arithmetical constraints. Both of these complementary approaches are applicable to the analysis of programs with numerical data.

Finally, members of the LIAFA (Zielonka and Serre) and LaBRI (Walukiewicz) teams are experts in games theory and its applications in modular verification and open systems verification. Existing collaborations : There are several existing collaborations between the teams of the project. The teams are partners in the (finishing) Persée (ACI sécurité) project. LIAFA and LSV are also partner in the RNTL project Averiles. LSV and LaBRI have strong collaboration links. Several members of the LaBRI team are former members of the LSV team.

[edit] Tasks and deliverables

[edit] Tasks

The work in the project will follow three parallel and complementary research tasks :

T1 Program models and abstraction techniques (automatic model extraction techniques from source code),

T2 Automatic verification techniques (based mainly on infinite-state symbolic model checking),

T3 Tool development and experimentations (targeting significant examples of software systems).

The three tasks are of course closely related and interdependent. The work in Task 1 aims at defining formal models of various significant classes of programs, and providing automatic techniques allowing to build such models starting from C source code. Models will be build at some abstraction level, and automatic abstraction refinement techniques (based on the analysis of counterexamples) will be applied. These refinement techniques depend of course of the results of the analysis techniques applied on the considered models and which are studied in Task 2.

Work in Task 2 concerns the definition of (exact/approximate) verification algorithms for infinite-state programs models (including techniques for the analysis of probabilistic models, and techniques for modular analysis). Analysis algorithms are based on symbolic representations of infinite sets of configurations. Such algorithms are either specific for particular classes of models for which they are guaranteed to terminate and to be exact, or based on generic techniques which can be applied to various classes of models, but which are either not guaranteed to terminate, or not exact (upper/under approximate), but accurate enough for the verification purpose.

In order to define more focused tasks (and corresponding working groups, we will define, within Task 2, the four following subtasks :

T2.1 Multi-threaded programs,

T2.2 Programs with (numerical) data and/or reference manipulation

T2.3 Infinite-state probabilistic models

T2.4 Infinite-state games and modular verification

Finally, work in Task 3 aims at implementing the algorithmic techniques developed in Task 1 and Task 2. Therefore Task 3 depends on the previous tasks, but it will also give important feedback and help in evaluating the applied approaches and discovering new efficient algorithmic techniques which are scalable and applicable to complex case studies.

[edit] Participation to tasks and collaborations

[edit] Participation to tasks

• Task 1 : In charge : LaBRI (Leroux). Participants : LIAFA, LaBRI
• Task 2.1 : In charge : LIAFA (Touili). Participants : LIAFA, LSV
• Task 2.2 : In charge : LSV (Demri). Participants : All teams
• Task 2.3 : In charge : LSV (Schnoebelen). Participants : LIAFA, LSV
• Task 2.4 : In charge : LSV (Zielonka). Participants : LIAFA, LaBRI
• Task 3 : In charge : LaBRI (Sutre). Participants : All teams

[edit] Intended collaborations

• LIAFA and LaBRI will collaborate for defining a CEGAR-based environment allowing to extract automatically abstract models from C code, apply (infinite-state) analysis and verification techniques (implemented in the tools TReX or FAST developed in the project), and refine by need the abstraction using symbolic counterexamples produced by the analysis.

• LSV and LaBRI will collaborate on the development of advanced techniques and new libraries (implemented in FAST) for automata-based representations of numerical constraints.

• LIAFA and LSV will collaborate on the problem of verifying multithreaded programs. They will also collaborate on the analysis of programs with data manipulation.

• LIAFA and LaBRI will collaborate on the problem of solving games for infinite-state programs models, and its application in modular verification of (sequential/multi-threaded) programs.

Other collaborations are expected between participants to the project on various research problems of common interest, in particular concerning the verification of programs with reference and pointer manipulation, and the verification of probabilistic models.

[edit] Deliverables

The deliverables correspond to the work plan defined in Section 3.2. They are given in Table 1, where R means report (conference and journal publications), and T means tool.

TAB. 1 – List of Deliverables

Title of Deliverable	Type	Main Partner	Other Partners	Date
Programs models	R	LaBRI	LIAFA	12
Sequential programs with data	R	LIAFA	LSV	12
Multithreaded boolean programs	R, T	LIAFA	LSV	12
Probabilistic sequential programs	Rt	LSV	LIAFA	12
Modular analysis of sequential programs	R	LIAFA	LaBRI	12
Model extraction	R, T	LaBRI	LIAFA	18
Multithreaded programs with data	R, T	LIAFA	LSV	24
Sequential programs with pointers	R	LSV	LaBRI, LIAFA	24
Probabilistic multithreaded programs	R	LSV	LIAFA	24
Modular analysis of multithreaded programs	R	LIAFA	LaBRI	24
Stochastic modular sequential programs	R	LIAFA	LaBRI	24
CEGAR environment	R, T	LaBRI	LIAFA	36
Multithreaded programs + pointers	R, T	LSV	LaBRI , LIAFA	36
Modular multithreaded programs + data	R, T	LIAFA	LSV	36
Stochastic modular multithreaded programs	R	LIAFA	LaBRI	36

[edit] Project organization and management

[edit] Working groups and project meetings

Participants to the project will meet frequently (at least each trimester) in small working groups related to each of the tasks and subtasks of the projects. Moreover, at least two global project meetings will be organized each year. External experts in our research domain (both form academia and from industry) will be invited to participate to these project meetings.

[edit] Coordination

The project will be coordinated by Ahmed Bouajjani, helped in this task by the two heads of the partner teams : Philippe Schnoebelen from LSV and Jérôme Leroux from LaBRI. Their task is to evaluate at each meeting the work progress w.r.t. the fixed work plan, and adapt the efforts and the research directions according to the difficulties which may appear, in order to reach the main objectives of the project.

[edit] Footnotes

1. ↑ In Java, for instance, one can use constructs such as synchronize, wait, notify, notifyAll, and the like.

[edit] References

1. S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254, Haifa, Israel, 1997. Springer Verlag. [GS97]
2. R. P. Kurshan. Computer-aided verification of coordinating processes : the automata-theoretic approach. In Princeton University Press, 1994. [Kur94]
3. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154-169, 2000. Extended version to appear in J. ACM. [CGJ+00]
4. S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In International Conference on Software Engineering (ICSE), pages 385-395, 2003. [CCG+03]
5. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Symposium on Principles of Programming Languages, pages 58-70, 2002. [HJMS02a]
6. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with BLAST. In LNCS 2648, volume 2648 of Lecture Notes in Computer Science, pages 235-239. Springer Verlag, 2003. Tool paper. [HJMS03]
7. T. A. Henzinger, R. Jhala, R. Majumdar, G. C. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In LNCS 2404, volume 2404 of Lecture Notes in Computer Science, pages 526-538. Springer Verlag, 2002. [HJM+02a]
8. T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. Lecture Notes in Computer Science, 2057, 2001. [BR01]
9. J. Esparza and S. Schwoon. A BDD-based model checker for recursive programs. In Proc. of CAV'01, number 2102 in Lecture Notes in Computer Science, pages 324-336. Springer-Verlag, 2001. [ES01]
10. Javier Esparza, Antonín Kucera, and Stefan Schwoon. Model-checking LTL with regular valuations for pushdown systems. Information and Computation, 186(2) :355-376, November 2003. [EKS03]
11. A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata : Application to Model Checking. In CONCUR'97. LNCS 1243, 1997. [BEM97]
12. Ahmed Bouajjani, Peter Habermehl, and Richard Mayr. Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science, 295(1-3) :85-106, February 2003. [BHM03]
13. G. Delzanno, J.-F. Raskin, and L. Van Begin. Attacking Symbolic State Explosion. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV 2001), volume 2102 of LNCS, pages 298-310. Springer, 2001. [DRB01]
14. G. Delzanno, J-F. Raskin, and L. Van Begin. Towards the Automated Verification of Multithreaded Java Programs. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2002), volume 2280 of LNCS, pages 173-187. Springer, 2002. [DRVB02]
15. Parosh Aziz Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science, 290(1) :241-264, 2003. [AJ03]
16. Parosh Aziz Abdulla, S. Purushothaman Iyer, and Aletta Nylén. Sat-solving the coverability problem for petri nets. Formal Methods in System Design, 24(1) :25-43, 2004. [AIN04]
17. Parosh Aziz Abdulla and Aletta Nylén. Better is better than well : On e efficient verification of infinite-state systems. In Proc. LICS'00 16th IEEE Int. Symp. on Logic in Computer Science, pages 132-140, 2000. [AN00]
18. A. Annichini, A. Bouajjani, and M.Sighireanu. Trex : A tool for reachability analysis of complex systems. In CAV 2001, 2001. [ABM01]
19. S. Bardin, A. Finkel, and J. Leroux. Faster acceleration of counter automata in practice. In Proc. 10th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2004), 2004. [BFL04a]
20. S. Bardin, A. Finkel, J. Leroux, L. Petrucci, and L. Worobel. Fast, users'manual. In http ://www.lsv.ens-cachan.fr/fast/, 2004. [BFL+04b]
21. S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. Fast : Fast accelereation of symbolic transition systems. In Proc. 15th Conf. Computer Aided Verification (CAV'2003), 2003. [BFLP03]
22. J. Leroux and G. Sutre. On flatness for 2-dimensional vector addition systems with states. In LNCS 3170, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer Verlag, 2004. [LS04]
23. G. Behrmann, P. Bouyer, E. Fleury, and K.G. Larsen. Static guards analysis in timed automata verification. In Proc. 9th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), Warsaw, Poland, Apr. 2003, volume 2619 of Lecture Notes in Computer Science, pages 254-277. Springer, 2003. [BBFL03]
24. Ahmed Bouajjani and Tayssir Touili. Reachability Analysis of Process Rewrite Systems. In Proc. 23rd Intern. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03), Mumbai, India, December 2003. LNCS 2914. [BT03]
25. A. Bouajjani, J. Esparza, and T. Touili. Reachability Analysis of Synchronised PA systems. In INFINITY'04. to appear in ENTCS, 2004. [BET04]
26. T. Touili. Dealing with communication for dynamic multithreaded recursive programs. In 1st VISSAS workshop, 2005. Invited Paper. [Tou05]
27. A. Bouajjani and T. Touili. On computing reachability sets of process rewrite systems. In Proc. 16th Int. Conf. on Rewriting Techniques and Applications (RTA'05), volume 3467 of Lecture Notes in Computer Science, April 2005. [BT05]
28. Ahmed Bouajjani, Markus Muller-Olm, and Tayssir Touili. Regular symbolic analysis of dynamic networks of pushdown systems. In CONCUR'05, LNCS, 2005. to appear. [BMOT05]
29. A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying programs with dynamic 1-selector-linked structures in regular model checking. Proceedings of TACAS'05, 2005. [BHMV05a]
30. Marius Bozga, Radu Iosif, and Yassine Lakhnech. On logics of aliasing. In Proceedings of 11th Static Analysis Symposium SAS'04, Verona, Italy, August 2004. [BIL04]
31. M. Bozga, R. Iosif, and Y. Lakhnech. Storeless semantics and alias logic. In Proceedings of ACM SIGPLAN 2003 Workshop on Partial Evaluation and Semantics Based Program Manipulation, PEPM'03, San Diego, California, pages 55-65. ACM Press, June 2003. [BIL03]
32. Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, and Tayssir Touili. Verifying concurrent message-passing c programs with recursive calls. In Holger Hermanns and Jens Palsberg, editors, TACAS, volume 3920 of Lecture Notes in Computer Science, pages 334-349. Springer, 2006. [CCK+06]
33. T. A. Henzinger, R. Jhala, R. Majumdar, G. C. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In Proc. 14th Int. Conf. Computer Aided Verification (CAV'2002), Copenhagen, Denmark, July 2002, volume 2404 of Lecture Notes in Computer Science, pages 526-538. Springer, 2002. [HJM+02b]
34. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proc. 29th ACM Symp. Principles of Programming Languages (POPL'2002), Portland, OR, USA, Jan. 2002, pages 58-70. ACM Press, 2002. [HJMS02b]
35. A. Finkel, B. Willems, and P. Wolper. A Direct Symbolic Approach to Model Checking Pushdown systems. Electronic Notes in Theoretical Computer Science, 9, 1997. [FWW97]
36. A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In Proc. of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'03, 2003. [BET03]
37. Ahmed Bouajjani, Peter Habermehl, and Tomás Vojnar. Abstract Regular Model Checking. In Proc. 16th Intern. Conf. on Computer Aided Verification (CAV'04), Boston, July 2004. LNCS 3114. [BHV04a]
38. Alain Finkel and Jérôme Leroux. How to compose Presburger-accelerations : Applications to broadcast protocols. In Manindra Agrawal and Anil Seth, editors, Proceedings of the 22nd Conference on Fundations of Software Technology and Theoretical Computer Science (FSTTCS'02), volume 2556 of Lecture Notes in Computer Science, pages 145-156, Kanpur, India, December 2002. Springer. [FL02]
39. S. Bardin and A. Finkel. Composition of accelerations to verify infinite heterogeneous systems. In Proc. 2nd Int. Symp. Automated Technology for Verification and Analysis (ATVA 2004), Taipei, Taiwan, Nov. 2004, volume 3299 of Lecture Notes in Computer Science, pages 248-262. Springer, 2004. [BF04]
40. A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying programs with dynamic 1-selector-linked structures in regular model checking. In TACAS05, Lecture Notes in Computer Science, pages 13-29. Springer, 2005. [BHMV05b]
41. Patrick Cousot and Nicholas Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL'78. ACM, 1978. [CH78]
42. B. Jeannet. Representing and approximating transfer functions in abstract interpretation of hetereogeneous datatypes. In Static Analysis Symposium, SAS'02, volume 2477 of LNCS, pages 52-68, Madrid (Spain)), September 2002. [Jea02]
43. B. Jeannet. partitionnement Dynamique dans l'Analyse de Relations Linéaires et Application à la Vérification de Programmes Synchrones. PhD thesis, Institut National Polytechnique de Grenoble, September 2000. [Jea00]
44. B. Jeannet. Dynamic partitioning in linear relation analysis. application to the verification of reactive systems. Formal Methods in System Design, 23(1) :5-37, July 2003. [Jea03]
45. S. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Programming Languages and Systems, 24(3) :217-298, 2002. [SRW02]
46. A. Loginov, T. Reps, and M. Sagiv. Abstraction Refinement for 3-Valued-Logic Analysis. Technical Report 1504, Computer Science Dept., University of Wisconsin, USA, 2004. [LRS04]
47. R. Manevich, E. Yahav, G. Ramalingam, and M. Sagiv. Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In Proc. of VMCAI'05. Springer, 2005. [MYRS05]
48. H.B.M. Jonkers. Abstract Storage Structures. In Algorithmic Languages. IFIP, 1981. [Jon81]
49. A. Deutsch. Interprocedural May-Alias Analysis for Pointers : Beyond k-Limiting. In Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI'94), Orlando, FL, USA, June 1994, pages 230-241. ACM Press, 1994. [Deu94]
50. A. Venet. Automatic analysis of pointer aliasing for untyped programs. Science of Computer Programming, 35(2) :223-248, 1999. [Ven99]
51. B. Jeannet, A. Loginov, T. Reps, and M. Sagiv. A relational approach to interprocedural shape analysis. Technical Report TR-1505, University of Wisconsin-Madison, April 2004. [JLRS04a]
52. B Jeannet, A. Loginov, T. Reps, and M. Sagiv. A relational approach to interprocedural shape analysis. In Static Analysis Symposium, SAS'04, volume 3148 of LNCS, Verona (Italy), August 2004. [JLRS04b]
53. Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, and Ahmed Bouajjani. A logic of reachable patterns in linked data-structures. In Luca Aceto and Anna Ingólfsdóttir, editors, FoSSaCS, volume 3921 of Lecture Notes in Computer Science, pages 94-110. Springer, 2006. [YRS+06]
54. P. Cousot and R. Cousot. Abstract interpretation : A unified model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM Symp. on Principles of Programming Languages, pages 238-252, 1977. [CC77]
55. B. Boigelot. The liEge automata-based symbolic handler. outil e` développéa l'ulg. Technical report, ULg, 2000. e [Boi00]
56. Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In Proc. 10th Int. Conf. on Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 88-97, Vancouver, July 1998. Springer-Verlag. [WB98]
57. A. Finkel, S. P. Iyer, and G. Sutre. Well-abstracted transition systems : Application to FIFO automata. Information and Computation, 181(1) :1-31, 2003. [FIS03]
58. Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, and Tayssir Touili. Regular model checking. In E. A. Emerson and A. P. Sistla, editors, Proceedings of the 12th International Conference on Computer-Aided Verification (CAV'00), volume 1855 of Lecture Notes in Computer Science, pages 403-418. Springer, 2000. [BJNT00]
59. A. Bouajjani. Languages, Rewriting systems, and Verification of Infinite-State Systems. In Proc. 28th Intern. Coll. on Automata, Languages and Programming (ICALP'01), Crete, Greece, July 2001. Lecture Notes in Computer Science 2076, Springer-Verlag. invited paper. [Bou01]
60. T. Touili. Regular model checking using widening techniques. Electronic Notes in Theoretical Computer Science, 50(3), 2001. [Tou01]
61. A. Bouajjani, A. Muscholl, and T. Touili. Permutation rewriting and algorithmic verification. In Proc. LICS'01 17th IEEE Int. Symp. on Logic in Computer Science. IEEE, 2001. [BMT01]
62. Ahmed Bouajjani and Tayssir Touili. Extrapolating Tree Transformations. In Proc. 14th Int. Conf. on Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, pages 539-554, 2002. [BT02]
63. B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proc. 6th Int. Conf. on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 55-67. Springer Verlag, 1994. [BW94]
64. B. Boigelot, A. Legay, and P. Wolper. Iterating transducers in the large. Lecture Notes in Computer Science, pages 223-235, 2003. [BLW03]
65. Ahmed Bouajjani, Peter Habermehl, and Tomás Vojnar. Abstract regular model checking. In Rajeev Alur and Doron Peled, editors, CAV, volume 3114 of Lecture Notes in Computer Science, pages 372-386. Springer, 2004. [BHV04b]
66. Ahmed Bouajjani, Peter Habermehl, Pierre Moro, and Tomás Vojnar. Verifying programs with dynamic 1-selector-linked structures in regular model checking. In Nicolas Halbwachs and Lenore D. Zuck, editors, TACAS, volume 3440 of Lecture Notes in Computer Science, pages 13-29. Springer, 2005. [BHMV05c]
67. A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract tree regular model checking of complex dynamic data structures. In SAS'06. to appear in LNCS, 2006. [BHRV06]
68. Igor Walukiewicz. Pushdown processes : Games and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, CAV, volume 1102 of Lecture Notes in Computer Science, pages 62-74. Springer, 1996. [Wal96]
69. Parosh Aziz Abdulla, Ahmed Bouajjani, and Julien d'Orso. Deciding monotonic games. In Matthias Baaz and Johann A. Makowsky, editors, CSL, volume 2803 of Lecture Notes in Computer Science, pages 1-14. Springer, 2003. [ABd03]
70. Javier Esparza and Kousha Etessami. Verifying probabilistic procedural programs. In Proceedings of FSTTCS 2004, volume 3328 of LNCS, Lecture Notes in Computer Science, pages 16-31, 2004. [EE04]
71. L. S. Shapley. Stochastic games. Proceedings Nat. Acad. of Science USA, 39 :1095-1100, 1953. [Sha53]
72. A. Neyman and S. Sorin, editors. Stochastic Games and Applications, volume 570 of NATO Science Series C, Mathematical and Physical Sciences. Kluwer Academic Publishers, 2004. [NS04]
73. A. Condon. The complexity of stochastic games. Information and Computation, 96 :203-224, 1992. [Con92]
74. C. Courcoubetis and M. Yannakakis. Markov decision processes and regular events. In ICALP'90, volume 443 of LNCS, pages 336-349. Springer, 1990. [CY90]
75. L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, december 1997. [dA97]
76. A.K. McIver and C.C. Morgan. Games, probability and the quantitative µ-calculus. In Proc. LPAR, volume 2514 of LNAI, pages 292-310. Springer, 2002. [MM02]
77. L. de Alfaro and R. Majumdar. Quantitative solution to omega-regular games. Journal of Computer and System Sciences, 68 :374-397, 2004. [dAM04]
78. W. Zielonka. Perfect-information stochastic parity games. In FOSSACS 2004, volume 2987 of LNCS, pages 499-513. Springer, 2004. [Zie04]