Advertisement

A Semi-automatic Proof of Strong Connectivity

  • Ran Chen
  • Jean-Jacques LévyEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)

Abstract

We present a formal proof of the classical Tarjan-1972 algorithm for finding strongly connected components in directed graphs. We use the Why3 system to express these proofs and fully check them by computer. The Why3-logic is a simple multi-sorted first-order logic augmented by inductive predicates. Furthermore it provides useful libraries for lists and sets. The Why3 system allows the description of programs in a Why3-ML programming language (a first-order programming language with ML syntax) and provides interfaces to various state-of-the-art automatic provers and to manual interactive proof-checkers (we use mainly Coq). We do not claim that this proof is new, although we could not find a formal proof of that algorithm in the literature. But one important point of our article is that our proof is here completely presented and human readable.

Notes

Acknowledgments

Thanks to the Why3 group at Inria-Saclay/LRI-Orsay for very valuable advices, to Cyril Cohen and Laurent Théry for their fantastic expertise in Coq proofs, to Claude Marché and the reviewers for many corrections.

References

  1. 1.
    Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Boston (1974)zbMATHGoogle Scholar
  2. 2.
    Appel, A.W.: Verified Functional Algorithms, August 2016. www.cs.princeton.edu/~appel/vfa/
  3. 3.
    Bobot, F., Filliâtre, J.C., Marché, C., Melquiond, G., Paskevich, A.: The Why3 platform, version 0.86.1. LRI, CNRS and Univ. Paris-Sud and INRIA Saclay, version 0.86.1 edn., May 2015. why3.lri.fr/download/manual-0.86.1.pdf
  4. 4.
    Bobot, F., Filliâtre, J.-C., Marché, C., Melquiond, G., Paskevich, A.: Preserving user proofs across specification changes. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 191–201. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54108-7_10. hal.inria.fr/hal-00875395 CrossRefGoogle Scholar
  5. 5.
    Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Let’s verify this with Why3. Softw. Tools Technol. Transf. (STTT) 17(6), 709–727 (2015). hal.inria.fr/hal-00967132
  6. 6.
    Charguéraud, A.: Program verification through characteristic formulae. In: Hudak, P., Weirich, S. (eds.) Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 321–332. ACM (2010). arthur.chargueraud.org/research/2010/cfml
  7. 7.
    Charguéraud, A.: Higher-order representation predicates in separation logic. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 3–14, CPP 2016. ACM, New York, January 2016Google Scholar
  8. 8.
    Charguéraud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP), August 2015Google Scholar
  9. 9.
    Chen, R., Lévy, J.J.: Full script of Tarjan SCC Why3 proof. Technical report, Iscas and Inria (2017). jeanjacqueslevy.net/why3/graph/abs/scct/2/scc.html
  10. 10.
    Chen, R., Lévy, J.J.: Une preuve formelle de l’algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe. In: JFLA (2017)Google Scholar
  11. 11.
    Clochard, M.: Preuves taillées en biseau. In: vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA). Gourette, France, January 2017. hal.inria.fr/hal-01404935
  12. 12.
    Cohen, C., Théry, L.: Full script of Tarjan SCC Coq/ssreflect proof. Technical report, Inria (2017). github.com/CohenCyril/tarjan
  13. 13.
    Coq Development Team: the coq 8.5 standard library. Technical report, Inria (2015). coq.inria.fr/distrib/current/stdlib
  14. 14.
    Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_8 CrossRefGoogle Scholar
  15. 15.
    Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Rapport de recherche RR-6455, INRIA (2008). hal.inria.fr/inria-00258384
  16. 16.
    Gonthier, G., et al.: Finite graphs in mathematical components (2012). ssr.msr-inria.inria.fr/~jenkins/current/Ssreflect.fingraph.html. The full library is available at www.msr-inria.fr/projects/mathematical-components-2
  17. 17.
    Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 523–536, POPL 2013. ACM, New York (2013). doi.acm.org/10.1145/2429069.2429131
  18. 18.
    Lammich, P., Neumann, R.: A framework for verifying depth-first search algorithms. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, pp. 137–146, CPP 2015. ACM, New York (2015). doi.acm.org/10.1145/2676724.2693165
  19. 19.
    Lévy, J.J.: Essays for the Luca Cardelli Fest. In: Simple Proofs of Simple Programs in Why3. Microsoft Research Cambridge, MSR-TR-2014-104 (2014)Google Scholar
  20. 20.
    Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: CADE (2003)Google Scholar
  21. 21.
    Poskitt, C.M., Plump, D.: Hoare logic for graph programs. In: VSTTE (2010)Google Scholar
  22. 22.
    Pottier, F.: Depth-first search and strong connectivity in Coq. In: Journées Francophones des Langages Applicatifs (JFLA 2015), January 2015Google Scholar
  23. 23.
    Raad, A., Hobor, A., Villard, J., Gardner, P.: Verifying concurrent graph algorithms. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 314–334. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47958-3_17 CrossRefGoogle Scholar
  24. 24.
    Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley, Boston (2011)Google Scholar
  25. 25.
    Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 77–87, PLDI 2015. ACM, New York (2015). doi.acm.org/10.1145/2737924.2737964
  26. 26.
    Tarjan, R.: Depth first search and linear graph algorithms. SIAM J. Comput. 1, 146–160 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Théry, L.: Formally-proven Kosaraju’s algorithm (2015). Inria report, Hal-01095533Google Scholar
  28. 28.
    Wengener, I.: A simplified correctness proof for a well-known algorithm computing strongly connected components. Inf. Process. Lett. 83(1), 17–19 (2002)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Why3 Development Team: Why3 gallery of programs. Technical report, CNRS and Inria (2016). toccata.lri.fr/gallery

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Inria SaclaySaclayFrance
  2. 2.ISCAS BeijingBeijingChina
  3. 3.Inria ParisParisFrance

Personalised recommendations