{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T17:16:56Z","timestamp":1771262216312,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,6,29]],"date-time":"2013-06-29T00:00:00Z","timestamp":1372464000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,3]]},"DOI":"10.1007\/s10817-013-9289-2","type":"journal-article","created":{"date-parts":[[2013,6,28]],"date-time":"2013-06-28T00:56:52Z","timestamp":1372381012000},"page":"241-273","source":"Crossref","is-referenced-by-count":17,"title":["A Framework for the Verification of Certifying Computations"],"prefix":"10.1007","volume":"52","author":[{"given":"Eyad","family":"Alkassar","sequence":"first","affiliation":[]},{"given":"Sascha","family":"B\u00f6hme","sequence":"additional","affiliation":[]},{"given":"Kurt","family":"Mehlhorn","sequence":"additional","affiliation":[]},{"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,6,29]]},"reference":[{"key":"9289_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-3-642-22110-1_7","volume-title":"Computer Aided Verification","author":"E Alkassar","year":"2011","unstructured":"Alkassar, E., B\u00f6hme, S., Mehlhorn, K., Rizkallah, C.: Verification of certifying computations. In: Computer Aided Verification. Lecture Notes in Computer Science, vol.\u00a06806, pp.\u00a067\u201382. Springer, New York (2011)"},{"key":"9289_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-642-14052-5_8","volume-title":"Interactive Theorem Proving","author":"M Armand","year":"2010","unstructured":"Armand, M., Gr\u00e9goire, B., Spiwack, A., Th\u00e9ry, L.: Extending Coq with imperative features and its application to SAT verification. In: Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 6172, pp. 83\u201398. Springer, New York (2010)"},{"key":"9289_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects. Lecture Notes in Computer Science, vol. 4111, pp. 364\u2013387. Springer, New York (2006)"},{"key":"9289_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-642-04468-7_16","volume-title":"Computer Safety, Reliability, and Security","author":"C Baumann","year":"2009","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Formal verification of a microkernel used in dependable software systems. In: Computer Safety, Reliability, and Security. Lecture Notes in Computer Science, vol.\u00a05775, pp. 187\u2013200. Springer, New York (2009)"},{"key":"9289_CR5","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: the Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: the Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, New York (2004)"},{"key":"9289_CR6","doi-asserted-by":"crossref","unstructured":"Blum, M., Kannan, S.: Designing programs that check their work. In: Symposium on Theory of Computing, pp.\u00a086\u201397. ACM (1989)","DOI":"10.1145\/73007.73015"},{"key":"9289_CR7","unstructured":"B\u00f6hme, S.: Proving theorems of higher-order logic with SMT solvers. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2012)"},{"key":"9289_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/978-3-540-71067-7_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S B\u00f6hme","year":"2008","unstructured":"B\u00f6hme, S., Leino, K.R.M., Wolff, B.: HOL-Boogie\u2014an interactive prover for the Boogie program-verifier. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol.\u00a05170, pp.\u00a0150\u2013166. Springer, New York (2008)"},{"issue":"1\u20132","key":"9289_CR9","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/s10817-009-9142-9","volume":"44","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Moskal, M., Schulte, W., Wolff, B.: HOL-Boogie\u2014an interactive prover-backend for the Verifying C Compiler. J. Autom. Reason. 44(1\u20132), 111\u2013144 (2010)","journal-title":"J. Autom. Reason."},{"key":"9289_CR10","doi-asserted-by":"crossref","unstructured":"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\u201315. Springer (1990)","DOI":"10.1007\/3-540-52885-7_75"},{"issue":"12","key":"9289_CR11","doi-asserted-by":"crossref","first-page":"1304","DOI":"10.1109\/12.641931","volume":"46","author":"JD Bright","year":"1997","unstructured":"Bright, J.D., Sullivan, G.F., Masson, G.M.: A formally verified sorting certifier. IEEE Trans. Comput. 46(12), 1304\u20131312 (1997)","journal-title":"IEEE Trans. Comput."},{"key":"9289_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Lecture Notes in Computer Science","author":"L Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 5170, pp. 134\u2013149. Springer, New York (2008)"},{"key":"9289_CR13","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Characteristic formulae for the verification of imperative programs. In: International Conference on Functional Programming, pp. 418\u2013430. ACM (2011)","DOI":"10.1145\/2034574.2034828"},{"key":"9289_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 5674, pp. 23\u201342. Springer, New York (2009)"},{"key":"9289_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/978-3-642-14808-8_18","volume-title":"Theoretical Aspects of Computing","author":"A Darbari","year":"2010","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: Theoretical Aspects of Computing. Lecture Notes in Computer Science, vol. 6255, pp. 260\u2013274. Springer, New York (2010)"},{"key":"9289_CR16","doi-asserted-by":"crossref","first-page":"125","DOI":"10.6028\/jres.069B.013","volume":"69B","author":"J Edmonds","year":"1965","unstructured":"Edmonds, J.: Maximum matching and a polyhedron with 0,1-vertices. J. Res. Natl. Bur. Stand. 69B, 125\u2013130 (1965)","journal-title":"J. Res. Natl. Bur. Stand."},{"key":"9289_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"JC Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590, pp. 173\u2013177. Springer, New York (2007)"},{"key":"9289_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science, vol.\u00a078. Springer, New York (1979)"},{"key":"9289_CR19","volume-title":"Introduction to HOL: a Theorem-Proving Environment for Higher-Order Logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: a Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"9289_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/978-3-642-32347-8_8","volume-title":"Lecture Notes in Computer Science","author":"D Greenaway","year":"2012","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: automatic verified abstraction of C. In: Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 7406, pp. 99\u2013115. Springer, New York (2012)"},{"issue":"6","key":"9289_CR21","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"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\u2013115 (2010)","journal-title":"Commun ACM"},{"key":"9289_CR22","first-page":"2","volume-title":"Software Engineering and Formal Methods","author":"D Leinenbach","year":"2005","unstructured":"Leinenbach, D., Paul, W.J., Petrova, E.: Towards the formal verification of a C0 compiler: code generation and implementation correctness. In: Software Engineering and Formal Methods, pp. 2\u201312. IEEE Computer Society Press, Los Alamitos (2005)"},{"issue":"2","key":"9289_CR23","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"9289_CR24","volume-title":"The LEDA Platform for Combinatorial and Geometric Computing","author":"K Mehlhorn","year":"1999","unstructured":"Mehlhorn, K., N\u00e4her, S.: The LEDA Platform for Combinatorial and Geometric Computing. Cambridge University Press, Cambridge (1999)"},{"key":"9289_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"LM Moura de","year":"2008","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, New York (2008)"},{"key":"9289_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014a Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014a Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, New York (2002)"},{"key":"9289_CR27","first-page":"210","volume-title":"Software Engineering and Formal Methods","author":"H Nivelle de","year":"2005","unstructured":"de\u00a0Nivelle, H., Piskac, R.: Verification of an off-line checker for priority queues. In: Software Engineering and Formal Methods, pp. 210\u2013219. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"9289_CR28","unstructured":"Nordhoff, B., Lammich, P.: Dijkstra\u2019s shortest path algorithm. Archive of Formal Proofs. http:\/\/afp.sourceforge.net\/entries\/Dijkstra_Shortest_Path.shtml (2012). Accessed 30 Jan 2012"},{"key":"9289_CR29","unstructured":"Norrish, M.: C formalised in HOL. PhD thesis, Computer Laboratory, University of Cambridge (1998)"},{"key":"9289_CR30","unstructured":"Noschinski, L.: Graph theory. Archive of Formal Proofs. http:\/\/afp.sf.net\/entries\/Graph_Theory.shtml , Formal proof development (2013). Accessed 28 Apr 2013"},{"key":"9289_CR31","unstructured":"Petrova, E.: Verification of the C0 compiler implementation on the source code level. PhD thesis, Saarland University, Saarbr\u00fccken (2007)"},{"key":"9289_CR32","unstructured":"Rizkallah, C.: Maximum cardinality matching. Archive of Formal Proofs. http:\/\/afp.sourceforge.net\/entries\/Max-Card-Matching.shtml (2011). Accessed 21 Jul 2011"},{"key":"9289_CR33","unstructured":"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"},{"key":"9289_CR34","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of sequential imperative programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"9289_CR35","first-page":"293","volume-title":"Engineering of Complex Computer Systems","author":"J Shi","year":"2012","unstructured":"Shi, J., He, J., Zhu, H., Fang, H., Huang, Y., Zhang, X.: ORIENTAIS: formal verified OSEK\/VDX real-time operating system. In: Engineering of Complex Computer Systems, pp.\u00a0293\u2013301. IEEE Computer Society Press, Los Alamitos (2012)"},{"key":"9289_CR36","first-page":"423","volume-title":"Fault-Tolerant Computing","author":"GF Sullivan","year":"1990","unstructured":"Sullivan, G.F., Masson, G.M.: Using certification trails to achieve software fault tolerance. In: Fault-Tolerant Computing, pp. 423\u2013431. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"9289_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 5674, pp. 452\u2013468. Springer, New York (2009)"},{"key":"9289_CR38","unstructured":"Verisoft XT: http:\/\/www.verisoftxt.de (2010). Accessed 20 May 2011"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9289-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9289-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9289-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,16]],"date-time":"2019-07-16T13:24:58Z","timestamp":1563283498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9289-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,29]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["9289"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9289-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6,29]]}}}