Advertisement

Progress on Certifying Algorithms

  • Kurt Mehlhorn
  • Pascal Schweitzer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6213)

Abstract

A certifying algorithm is an algorithm that produces with each output, a certificate or witness (easy-to-verify proof) that the particular output has not been compromised by a bug. A user of a certifying program P (= the implementation of a certifying algorithm) inputs x, receives an output y and a certificate w, and then checks, either manually or by use of a checking program, that w proves that y is a correct output for input x. In this way, he/she can be sure of the correctness of the output without having to trust P. We refer the reader to the recent survey paper [9] for a detailed discussion of certifying algorithms.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Edmonds, J.: Maximum matching and a polyhedron with 0,1 - vertices. Journal of Research of the National Bureau of Standards 69B, 125–130 (1965)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Edmonds, J.: Paths, trees, and flowers. Canadian Journal on Mathematics, 449–467 (1965)Google Scholar
  3. 3.
    Elmasry, A., Mehlhorn, K., Schmidt, J.M.: A Linear Time Certifying Triconnectivity Algorithm for Hamiltonian Graphs. Available at the authors home pages (March 2010)Google Scholar
  4. 4.
    Elmasry, A., Mehlhorn, K., Schmidt, J.M.: Every DFS-Tree of a 3-Connected Graph Contains a Contractible Edge. Available at the authors home pages (February 2010)Google Scholar
  5. 5.
    Gutwenger, C., Mutzel, P.: A linear time implementation of SPQR-trees. In: Marks, J. (ed.) GD 2000. LNCS, vol. 1984, pp. 77–90. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Hopcroft, J.E., Tarjan, R.E.: Dividing a graph into triconnected components. SIAM Journal of Computing 2(3), 135–158 (1973)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Isabelle theorem prover, http://isabelle.in.tum.de/
  8. 8.
    Kriesell, M.: A survey on contractible edges in graphs of a prescribed vertex connectivity. Graphs and Combinatorics, 1–33 (2002)Google Scholar
  9. 9.
    Mehlhorn, K., McConnell, R., Näher, S., Schweitzer, P.: Certifying Algorithms. Available at the first author’s homepage and submitted for publicationGoogle Scholar
  10. 10.
    Miller, G.L., Ramachandran, V.: A new graph triconnectivity algorithm and its parallelization. Combinatorica 12(1), 53–76 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Nagamochi, H., Ibaraki, T.: A linear-time algorithm for finding a sparse k-connected spanning subgraph of a k-connected graph. Algorithmica 7, 583–596 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Schmidt, J.M.: Construction sequences and certifying 3-connectedness. In: 27th International Symposium on Theoretical Aspects of Computer Science (STACS 2010), Nancy, France (2010), http://page.mi.fu-berlin.de/jeschmid/pub
  13. 13.
    Tutte, W.: A theory of 3-connected graphs. Indag. Math. 23, 441–455 (1961)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    VCC, a mechanical verifier for concurrent C programs, http://vcc.codeplex.com/

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Kurt Mehlhorn
    • 1
  • Pascal Schweitzer
    • 1
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany

Personalised recommendations