{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:46:38Z","timestamp":1767926798131,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642277047","type":"print"},{"value":"9783642277054","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27705-4_2","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T17:18:06Z","timestamp":1327511886000},"page":"2-17","source":"Crossref","is-referenced-by-count":17,"title":["A Certified Multi-prover Verification Condition Generator"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Herms","sequence":"first","affiliation":[]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Monate","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book, assigning programs to meaning. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., DeLine, R., Jacobs, B., Chang, B.-Y.E., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"2_CR4","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, version 1.4 (2009), http:\/\/frama-c.cea.fr\/acsl.html"},{"key":"2_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)"},{"key":"2_CR6","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroc\u0142aw, Poland (August 2011)"},{"issue":"3","key":"2_CR7","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT)\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"2_CR8","unstructured":"Chlipala, A.: Certified Programming with Dependent Types. MIT Press (2011), http:\/\/adam.chlipala.net\/cpdt\/"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/1596550.1596565","volume-title":"ICFP","author":"A.J. Chlipala","year":"2009","unstructured":"Chlipala, A.J., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: Hutton, G., Tolmach, A.P. (eds.) ICFP, pp. 79\u201390. ACM, Edinburgh (2009)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting eSC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contract-based modular verification of concurrent C. In: 31st International Conference on Software Engineering Companion, ICSE 2009, Vancouver, Canada, May 16-24, pp. 429\u2013430. IEEE Comp. Soc. Press (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"issue":"4","key":"2_CR12","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1017\/S095679680200446X","volume":"13","author":"J.-C. Filli\u00e2tre","year":"2003","unstructured":"Filli\u00e2tre, J.-C.: Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming\u00a013(4), 709\u2013745 (2003)","journal-title":"Journal of Functional Programming"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-Prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"2_CR15","unstructured":"Herms, P.: Certification of a chain for deductive program verification. In: Bertot, Y. (ed.) 2nd Coq Workshop, Satellite of ITP 2010 (2010)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Herms, P., March\u00e9, C., Monate, B.: A certified multi-prover verification condition generator. Research Report 7793, INRIA (2011), http:\/\/hal.inria.fr\/hal-00639977\/en\/","DOI":"10.1007\/978-3-642-27705-4_2"},{"issue":"2","key":"2_CR17","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1093\/comjnl\/38.2.131","volume":"38","author":"P.V. Homeier","year":"1995","unstructured":"Homeier, P.V., Martin, D.F.: A mechanically verified verification condition generator. The Computer Journal\u00a038(2), 131\u2013141 (1995)","journal-title":"The Computer Journal"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/3-540-61511-3_81","volume-title":"Automated Deduction - Cade-13","author":"P.V. Homeier","year":"1996","unstructured":"Homeier, P.V., Martin, D.F.: Mechanical Verification of Mutually Recursive Procedures. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 201\u2013215. Springer, Heidelberg (1996)"},{"issue":"4","key":"2_CR19","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR20","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X. Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput.\u00a0207, 284\u2013304 (2009)","journal-title":"Inf. Comput."},{"key":"2_CR21","unstructured":"Lescuyer, S.: Formalisation et d\u00e9veloppement d\u2019une tactique r\u00e9flexive pour la d\u00e9monstration automatique en Coq. Th\u00e8se de doctorat, Universit\u00e9 Paris-Sud (2011)"},{"issue":"1-2","key":"2_CR22","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java\/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming\u00a058(1-2), 89\u2013106 (2004), http:\/\/krakatoa.lri.fr","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Reasoning with the awkward squad. In: Proceedings of ICFP 2008(2008)","DOI":"10.1145\/1411204.1411237"},{"key":"2_CR24","unstructured":"Norrish, M.: C Formalised in HOL. PhD thesis, University of Cambridge (November 1998)"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1798","DOI":"10.1007\/3-540-48118-4_45","volume-title":"FM\u201999 - Formal Methods","author":"F. Randimbivololona","year":"1999","unstructured":"Randimbivololona, F., Souyris, J., Baudin, P., Pacalet, A., Raguideau, J., Schoen, D.: Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1798\u20131815. Springer, Heidelberg (1999)"},{"key":"2_CR26","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":"2_CR27","volume-title":"Formal Verification of Object-Oriented Software, Papers Presented at the International Conference","author":"M. Wagner","year":"2010","unstructured":"Wagner, M., Bormer, T.: Testing a verifying compiler. In: Beckert, B., March\u00e9, C. (eds.) Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Karlsruhe Reports in Informatics, Paris (2010), http:\/\/digbib.ubka.uni-karlsruhe.de\/volltexte\/1000019083"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,27]],"date-time":"2021-12-27T00:44:46Z","timestamp":1640565886000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}