High-Quality Abstractions for the Verification of Asynchronous Distributed Systems

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

Scientific context

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.

Goals

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

References

  1. S. Bardin, A. Finkel, J. Leroux, L. Petrucci. FAST: Acceleration from Theory to Practice. Software Tools for Technology Transfer, 10(5): 401-424, 2008.
  2. Y.-F. Chen, A. Farzan, E. M. Clarke, Y.-K. Tsay, B.-Y. Wang. Learning Minimal Separating DFA’s for Compositional Verification. In Proc. TACAS'09, LNCS 5505, pages 31–45. Springer, 2009.
  3. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM, 50(5): 752-794, 2003.
  4. P. Cousot, R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. POPL'79, pages 269–282. ACM Press, 1979.
  5. G. Geeraerts, A. Heußner, J.-F. Raskin. Queue-Dispatch Asynchronous Systems. In Proc. ACSD'13, pages 150–159. IEEE, 2013
  6. A. Lal, T. W. Reps. Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. Formal Methods in System Design, 35(1): 73-97, 2009.
  7. J. Leroux, G. Sutre. Accelerated Data-Flow Analysis. In Proc. SAS'07, LNCS 4634, pages 184–199. Springer, 2007.
  8. T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Lazy Abstraction. In Proc. POPL'02, pages 58–70. ACM, 2002.
  9. A. Heussner, T. Le Gall, and G. Sutre. McScM: A General Framework for the Verification of Communicating Machines. In Proc. TACAS'12, LNCS 7214, pages 478–484. Springer, 2012.
  10. A. Heussner, T. Le Gall, and G. Sutre. Safety Verification of Communicating One-Counter Machines. In Proc. FSTTCS'12, LIPIcs 18, pages 224–235. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012.
  11. P. Ganty, R. Majumdar. Algorithmic Verification of Asynchronous Programs. ACM Trans. Program. Lang. Syst., 34(1): 6, 2012.
  12. P. Rümmer, H. Hojjat, V. Kuncak. Disjunctive Interpolants for Horn-Clause Verification. In Proc. CAV'13, LNCS 8044, pages 347–363. Springer, 2013.
  13. K. Sen, M. Viswanathan. Model Checking Multithreaded Programs with Asynchronous Atomic Methods. In Proc. CAV'06, LNCS 4144, pages 300–314. Springer, 2006.