×

A framework for the verification of certifying computations. (English) Zbl 1314.68180

Summary: Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current automatic verification tools and usually involves intricate mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for such a witness is usually much simpler than the original algorithm – yet it is all the user has to trust. The verification of checkers is feasible with current tools and leads to computations that can be completely trusted. We describe a framework to seamlessly verify certifying computations. We use the automatic verifier VCC for establishing the correctness of the checker and the interactive theorem prover Isabelle/HOL for high-level mathematical properties of algorithms. We demonstrate the effectiveness of our approach by presenting the verification of typical examples of the industrial-level and widespread algorithmic library LEDA.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Alkassar, E.; Böhme, S.; Mehlhorn, K.; Rizkallah, C., Verification of certifying computations, No. 6806, 67-82 (2011), New York
[2] Armand, M.; Grégoire, B.; Spiwack, A.; Théry, L., Extending Coq with imperative features and its application to SAT verification, No. 6172, 83-98 (2010), New York · Zbl 1291.68318
[3] Barnett, M.; Chang, BYE; DeLine, R.; Jacobs, B.; Leino, KRM, Boogie: a modular reusable verifier for object-oriented programs, No. 4111, 364-387 (2006), New York
[4] Baumann, C.; Beckert, B.; Blasum, H.; Bormer, T., Formal verification of a microkernel used in dependable software systems, No. 5775, 187-200 (2009), New York
[5] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development—Coq’Art: the Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, New York (2004) · Zbl 1069.68095
[6] Blum, M., Kannan, S.: Designing programs that check their work. In: Symposium on Theory of Computing, pp. 86-97. ACM (1989) · Zbl 0886.68046
[7] Böhme, S.: Proving theorems of higher-order logic with SMT solvers. PhD thesis, Technische Universität München (2012) · Zbl 1246.83140
[8] Böhme, S.; Leino, KRM; Wolff, B., HOL-Boogie—an interactive prover for the Boogie program-verifier, No. 5170, 150-166 (2008), New York · Zbl 1165.68399
[9] Böhme, S., Moskal, M., Schulte, W., Wolff, B.: HOL-Boogie—an interactive prover-backend for the Verifying C Compiler. J. Autom. Reason. 44(1-2), 111-144 (2010) · Zbl 1185.68211
[10] Boyer, R.S., Moore, J.S.: A theorem prover for a computational logic. In: Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 449, pp. 1-15. Springer (1990) · Zbl 0708.68060
[11] Bright, J.D., Sullivan, G.F., Masson, G.M.: A formally verified sorting certifier. IEEE Trans. Comput. 46(12), 1304-1312 (1997)
[12] Bulwahn, L.; Krauss, A.; Haftmann, F.; Erkök, L.; Matthews, J., Imperative functional programming with Isabelle/HOL, No. 5170, 134-149 (2008), New York · Zbl 1165.68352
[13] Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: International Conference on Functional Programming, pp. 418-430. ACM (2011) · Zbl 1323.68366
[14] Cohen, E.; Dahlweid, M.; Hillebrand, M.; Leinenbach, D.; Moskal, M.; Santen, T.; Schulte, W.; Tobies, S., VCC: a practical system for verifying concurrent C, No. 5674, 23-42 (2009), New York
[15] Darbari, A.; Fischer, B.; Marques-Silva, J., Industrial-strength certified SAT solving through verified SAT proof checking, No. 6255, 260-274 (2010), New York
[16] Edmonds, J.: Maximum matching and a polyhedron with 0,1-vertices. J. Res. Natl. Bur. Stand. 69B, 125-130 (1965) · Zbl 0141.21802
[17] Filliâtre, JC; Marché, C., The Why/Krakatoa/Caduceus platform for deductive program verification, No. 4590, 173-177 (2007), New York
[18] Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science, vol. 78. Springer, New York (1979) · Zbl 0421.68039
[19] Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: a Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993) · Zbl 0779.68007
[20] Greenaway, D.; Andronick, J.; Klein, G., Bridging the gap: automatic verified abstraction of C, No. 7406, 99-115 (2012), New York · Zbl 1360.68751
[21] Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. Commun ACM 53(6), 107-115 (2010)
[22] Leinenbach, D.; Paul, WJ; Petrova, E., Towards the formal verification of a C0 compiler: code generation and implementation correctness, 2-12 (2005), Los Alamitos
[23] McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119-161 (2011) · Zbl 1298.68289
[24] Mehlhorn, K., Näher, S.: The LEDA Platform for Combinatorial and Geometric Computing. Cambridge University Press, Cambridge (1999) · Zbl 0976.68156
[25] Moura, LM; Bjørner, N., Z3: an efficient SMT solver, No. 4963, 337-340 (2008), New York
[26] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—a Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, New York (2002) · Zbl 0994.68131
[27] Nivelle, H.; Piskac, R., Verification of an off-line checker for priority queues, 210-219 (2005), Los Alamitos
[28] Nordhoff, B., Lammich, P.: Dijkstra’s shortest path algorithm. Archive of Formal Proofs. http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml (2012). Accessed 30 Jan 2012 · Zbl 1291.68318
[29] Norrish, M.: C formalised in HOL. PhD thesis, Computer Laboratory, University of Cambridge (1998)
[30] Noschinski, L.: Graph theory. Archive of Formal Proofs. http://afp.sf.net/entries/Graph_Theory.shtml, Formal proof development (2013). Accessed 28 Apr 2013
[31] Petrova, E.: Verification of the C0 compiler implementation on the source code level. PhD thesis, Saarland University, Saarbrücken (2007)
[32] Rizkallah, C.: Maximum cardinality matching. Archive of Formal Proofs. http://afp.sourceforge.net/entries/Max-Card-Matching.shtml (2011). Accessed 21 Jul 2011 · Zbl 1185.68211
[33] Rizkallah, C.: An axiomatic characterization of the single-source shortest path problem. Archive of Formal Proofs. http://afp.sf.net/entries/ShortestPath.shtml, Formal proof development (2013). Accessed 22 May 2013
[34] Schirmer, N.: Verification of sequential imperative programs in Isabelle/HOL. PhD thesis, Technische Universität München (2006) · Zbl 1108.68410
[35] Shi, J.; He, J.; Zhu, H.; Fang, H.; Huang, Y.; Zhang, X., ORIENTAIS: formal verified OSEK/VDX real-time operating system, 293-301 (2012), Los Alamitos
[36] Sullivan, GF; Masson, GM, Using certification trails to achieve software fault tolerance, 423-431 (1990), Los Alamitos
[37] Thiemann, R.; Sternagel, C., Certification of termination proofs using CeTA, No. 5674, 452-468 (2009), New York · Zbl 1252.68265
[38] Verisoft XT: http://www.verisoftxt.de (2010). Accessed 20 May 2011
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.