Skip to main content
SpringerLink
Log in

From algorithms to working programs: On the use of program checking in LEDA

  • Invited Papers
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1998 (MFCS 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1450))

Abstract

We report on the use of program checking in the LEDA library of efficient data types and algorithms.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. N.M. Amato and M.C. Loui. Checking linked data structures. In Proceedings of the 24th Annual International Symposium on Fault-Tolerant Computing, pages 164–173, 1994.

    Google Scholar 

  2. M. Blum and S. Kannan. Programs That Check Their Work. In Proc. of the 21th Annual ACM Symp. on Theory of Computing, 1989.

    Google Scholar 

  3. K.S. Booth and G.S. Luecker. Testing for the Consecutive Ones Property, Interval Graphs, and Graph Planarity Using PQ-tree Algorithms. Journal of Comp. and Sys. Sciences, 13:335–379, 1976.

    MATH  Google Scholar 

  4. M. Blum, M. Luby, and R. Rubinfeld. Self-testing/correcting with applications to numerical problems. In Proc. 22nd Annual ACM Symp. on Theory of Computing, pages 73–83, 1990.

    Google Scholar 

  5. J. D. Bright and G. F. Sullivan. Checking mergeable priority queues. In Proceedings of the 24th Annual International Symposium on Fault-Tolerant Computing, pages 144–153, Los Alamitos, CA, USA, June 1994. IEEE Computer Society Press.

    Google Scholar 

  6. J. D. Bright and G. F. Sullivan. On-line error monitoring for several data structures. In FTCS-25: 25th International Symposium on Fault Tolerant Computing Digest of Papers, pages 392–401, Pasadena, California, 1995.

    Google Scholar 

  7. J. D. Bright, G. F. Sullivan, and G. M. Masson. Checking the integrity of trees. In FTCS-25: 25th International Symposium on Fault Tolerant Computing Digest of Papers, pages 402–413, Pasadena, California, 1995.

    Google Scholar 

  8. J.D. Bright, G. F. Sullivan, and G. M. Masson. A formally verified sorting certifier. IEEE Transactions on Computers, 46(12):1304–1312, 1997.

    Article  Google Scholar 

  9. M. Blum and H. Wasserman. Reflections on the pentium division bug. IEEE Trans. Comput., 45(4):385–393, April 1996.

    Article  MATH  Google Scholar 

  10. Norishige Chiba, Takao Nishizeki, Shigenobu Abe, and Takao Ozawa. A linear algorithm for embedding planar graphs using PQ-trees. Journal of Computer and System Sciences, 30(1):54–76, February 1985.

    Article  MATH  MathSciNet  Google Scholar 

  11. J. Edmonds. Maximum matching and a polyhedron with 0,1 — vertices. Journal of Research of the National Bureau of Standards, 69B:125–130, 1965.

    MathSciNet  Google Scholar 

  12. H.N. Gabow. An efficient implementation of Edmond's algorithm for maximum matching on graphs. JACM, 23:221–234, 1976.

    Article  MATH  MathSciNet  Google Scholar 

  13. C. Hundack, K. Mehlhorn, and S. Näher. A Simple Linear Time Algorithm for Identifying Kuratowski Subgraphs of Non-Planar Graphs. Manuscript, 1996.

    Google Scholar 

  14. J.E. Hopcroft and R.E. Tarjan. Efficient planarity testing. Journal of the ACM, 21:549–568, 1974.

    Article  MATH  MathSciNet  Google Scholar 

  15. A. Karabeg. Classification and detetection of obstructions to planarity. Linear and Multilinear Algebra, 26:15–38, 1990.

    MATH  MathSciNet  Google Scholar 

  16. C. Kuratwoski. Sur le problème the courbes guaches en topologie. Fundamenta Mathematicae, 15:271–283, 1930.

    Google Scholar 

  17. A. Lempel, S. Even, and I. Cederbaum. An Algorithm for Planarity Testing of Graphs. In P. Rosenstiehl, editor, Theory of Graphs, International Symposium, Rome, pages 215–232, 1967.

    Google Scholar 

  18. K. Mehlhorn and P. Mutzel. On the Embedding Phase of the Hopcroft and Tarjan Planarity Testing Algorithm. Algorithmica, 16(2):233–242, 1995.

    Article  MathSciNet  Google Scholar 

  19. K. Mehlhorn and S. Näher. LEDA, a platform for combinatorial and geometric computing. Communications of the ACM, 38:96–102, 1995.

    Article  Google Scholar 

  20. K. Mehlhorn and S. Näher. The LEDA Platform for Combinatorial and Geometric Computing. Cambridge University Press, 1998. Draft versions of some chapters are available at http://www.mpi-sb.mpg.de/~mehlhorn.

    Google Scholar 

  21. K. Mehlhorn, S. Näher, T. Schilz, S. Schirra, M. Seel, R. Seidel, and Ch. Uhrig. Checking Geometric Programs or Verification of Geometric Structures. In Proc. of the 12th Annual Symposium on Computational Geometry, pages 159–165, 1996.

    Google Scholar 

  22. Kurt Mehlhorn, S. Näher, and Ch. Uhrig. The LEDA User Manual (Version R 3.5). Technical report, Max-Planck-Institut für Informatik, 1997. http://www.mpi-sb.mpg.de/LEDA/leda.html.

    Google Scholar 

  23. T. Nishizeki and N. Chiba. Planar Graphs: Theory and Algorithms. Annals of Discrete Mathematics (32). North-Holland Mathematics Studies, 1988.

    Google Scholar 

  24. O.Devillers, G. Liotta, F.P. Preparata, and R. Tamassia. Checking the convexity of polytopes and the planarity of subdivisions. Technical report, Center for Geometric Computing, Department of Computer Science, Brown University, 1997.

    Google Scholar 

  25. G. F. Sullivan and G. M. Masson. Using certification trails to achieve software fault tolerance. In Brian Randell, editor, Proceedings of the 20th International Symposium on Fault-Tolerant Computing (FTCS '90), pages 423–433, Newcastle upon Tyne, UK, June 1990. IEEE Computer Society Press.

    Google Scholar 

  26. G. F. Sullivan and G. M. Masson. Certification trails for data structures. In Proceedings of the 21st International Symposium on Fault-Tolerant Computing, pages 240–247, 1991.

    Google Scholar 

  27. G.F. Sullivan, D.S. Wilson, and G.M. Masson. Certification of computational results. IEEE Transactions on Computers, 44(7):833–847, 1995.

    Article  MATH  Google Scholar 

  28. Hal Wasserman and Manuel Blum. Software reliability via run-time result-checking. Journal of the ACM, 44(6):826–849, November 1997.

    Article  MATH  MathSciNet  Google Scholar 

  29. S.G. Williamson. Depth-First Search and Kuratowski Subgraphs. JACM, 31(4):681–693, 1984.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Insitut für Informatik, Im Stadtwald, D-66123, Saarbrücken, Germany

    Kurt Mehlhorn

  2. FB Mathematik und Informatik, Martin-Luther-Universität Halle-Wittenberg, Kurt-Mothes-Str. 1, D-06099, Halle (Saale), Germany

    Stefan Näher

Authors
  1. Kurt Mehlhorn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Näher
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Luboš Brim Jozef Gruska Jiří Zlatuška

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mehlhorn, K., Näher, S. (1998). From algorithms to working programs: On the use of program checking in LEDA. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055759

Download citation

  • DOI: https://doi.org/10.1007/BFb0055759

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64827-7

  • Online ISBN: 978-3-540-68532-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation