Advisors: | Jérôme Leroux and Grégoire Sutre |
E-mail: | {Jerome.Leroux, Gregoire.Sutre}@labri.fr |
Team: | Formal Methods / Modeling and Verification |
Location: | LaBRI (Computer Science Research Laboratory of Bordeaux), University of Bordeaux, France |
Keywords: | Verification, Asynchronous Systems, Infinite-State Systems, Acceleration, Abstract Interpretation, CEGAR, Interpolation, Learning |
Asynchronous distributed systems (such as multi-threaded programs, client/server applications, …) are ubiquitous nowadays, but they are also notoriously difficult to design correctly. This is due to the complex (and sometimes unforeseen) interactions resulting from asynchronous communications. Therefore, there is a growing need for automatic verification tools capable of analyzing such systems. This need is amplified with the current development of multi-core architectures. The last decade has seen a lot of research efforts in this field, e.g., [2, 5, 6, 9, 10, 11, 13].
The verification of safety properties reduces to the effective computation of inductive invariants. Abstract interpretation [4] provides a general framework for computing these invariants. Basically, in this approach a concrete system is abstracted away into an abstract one that can be automatically verified. If the abstract system is correct, then by construction, the concrete system is known to be correct. Since the converse is not true, when the abstract system is incorrect, the abstraction must be refined.
The CEGAR approach, for Counter Example Guided Abstract Refinement [3, 8], provides a general way for improving too coarse abstractions. Basically, the CEGAR approach relies on a finite set of predicates that are computed inductively. New predicates are needed when the abstraction provided by the set of predicates computed so far is not precise enough.
Abstract interpretation and CEGAR both compute invariants but with different priorities. The former puts the emphasis on the efficiency at the cost of precision of the analysis, while the later cares about the quality of the analysis. In practice, the convergence of the CEGAR approach relies deeply on the quality of the abstraction.
The computation of high-quality abstractions is a challenging problem. Recently, the Craig interpolation technique has provided promising results for the verification of sequential programs. Intuitively, from a proof witnessing the impreciseness of an abstraction, new predicates are computed. Extending this technique to asynchronous distributed systems is a challenging problem. State-of-the-art model-checkers (e.g., CSeq) for multi-threaded programs first apply a sequentialization up to a fixed number of context switches [6], and then apply classical verification techniques on the resulting sequential program.
This proposal aims at providing new techniques for computing high-quality abstractions for the analysis of asynchronous distributed systems based on various frameworks : program transformation [6], assume-guarantee [2], interpolation abstraction [12], abstract acceleration [1, 7], learning [2].