{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T02:20:12Z","timestamp":1764210012737,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357459"},{"type":"electronic","value":"9783642357466"}],"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-35746-6_3","type":"book-chapter","created":{"date-parts":[[2012,12,13]],"date-time":"2012-12-13T20:38:40Z","timestamp":1355431120000},"page":"45-95","source":"Crossref","is-referenced-by-count":19,"title":["Introduction to the Coq Proof-Assistant for Practical Software Verification"],"prefix":"10.1007","author":[{"given":"Christine","family":"Paulin-Mohring","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Technical report, Microsoft Research - Inria Joint Centre (MSR - INRIA) (2011), \n                  \n                    http:\/\/hal.inria.fr\/inria-00258384"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M. Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A Modular Integration of SAT\/SMT Solvers to Coq through Proof Witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 135\u2013150. Springer, Heidelberg (2011)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 83\u201398. Springer, Heidelberg (2010)"},{"key":"3_CR4","unstructured":"Asperti, A., Coen, C.S., et al.: Matita, \n                  \n                    http:\/\/matita.cs.unibo.it\/"},{"key":"3_CR5","unstructured":"Aspinall, D.: Proof general, \n                  \n                    http:\/\/proofgeneral.inf.ed.ac.uk\/"},{"issue":"8","key":"3_CR6","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P. Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Science of Computer Programming\u00a074(8), 568\u2013589 (2009)","journal-title":"Science of Computer Programming"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90\u2013101. ACM (2009), \n                  \n                    http:\/\/www.msr-inria.inria.fr\/projects\/sec\/certicrypt","DOI":"10.1145\/1480881.1480894"},{"key":"3_CR8","unstructured":"Bertot, Y.: Coq in a Hurry. Technical report, MARELLE - INRIA Sophia Antipolis (May 2010)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer (2004), \n                  \n                    http:\/\/www.labri.fr\/perso\/casteran\/CoqArt","DOI":"10.1007\/978-3-662-07964-5"},{"key":"3_CR10","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)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-14052-5_12","volume-title":"Interactive Theorem Proving","author":"S. Boldo","year":"2010","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Formal Proof of a Wave Equation Resolution Scheme: The Method Error. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 147\u2013162. Springer, Heidelberg (2010), \n                  \n                    http:\/\/hal.inria.fr\/hal-00649240\/PDF\/RR-7826.pdf"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Boldo, S., Melquiond, G.: Flocq: A unified library for proving floating-point algorithms in Coq. In: Antelo, E., Hough, D., Ienne, P. (eds.) Proceedings of the 20th IEEE Symposium on Computer Arithmetic, T\u00fcbingen, Germany, pp. 243\u2013252 (2011), \n                  \n                    http:\/\/flocq.gforge.inria.fr\/","DOI":"10.1109\/ARITH.2011.40"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Bolignano, D.: An approach to the formal verification of cryptographic protocols. In: CCS 1996 Proceedings of the 3rd ACM Conference on Computer and Communications Security (1996)","DOI":"10.1145\/238168.238196"},{"key":"3_CR14","unstructured":"Chetali, B., Nguyen, Q.-H.: About the world-first smart card certificate with EAL7 formal assurances. In: Slides 9th ICCC, Jeju, Korea (September 2008), \n                  \n                    www.commoncriteriaportal.org\/iccc\/9iccc\/pdf\/B2404.pdf"},{"key":"3_CR15","unstructured":"Chlipala, A.: Certified Programming with Dependent Types. MIT Press (2011), \n                  \n                    http:\/\/adam.chlipala.net\/cpdt\/"},{"key":"3_CR16","unstructured":"Constable, R.L., Bates, J.L., Kreitz, C., van Renesse, R., et al.: Prl: Proof\/program refinement logic, \n                  \n                    http:\/\/www.cs.cornell.edu\/info\/projects\/nuprl\/"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Contejean, E., Paskevich, A., Urbain, X., Courtieu, P., Pons, O., Forest, J.: A3pat, an approach for certified automated termination proofs. In: Gallagher, J.P., Voigtl\u00e4nder, J. (eds.) Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010, pp. 63\u201372. ACM (2010)","DOI":"10.1145\/1706356.1706370"},{"key":"3_CR18","unstructured":"Coquand, C., Coquand, T., Nurell, U., et al.: Agda, \n                  \n                    http:\/\/wiki.portal.chalmers.se\/agda"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/3-540-15983-5_13","volume-title":"EUROCAL \u201985. European Conference on Computer Algebra. Linz, Austria, April 1-3, 1985. Proceedings","author":"T. Coquand","year":"1985","unstructured":"Coquand, T., Huet, G.: Constructions: a Higher-order Proof System for Mechanizing Mathematics. In: Buchberger, B. (ed.) ISSAC 1985 and EUROCAL 1985. LNCS, vol.\u00a0203, pp. 151\u2013184. Springer, Heidelberg (1985)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Daumas, M., Melquiond, G.: Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software\u00a037(1) (2010)","DOI":"10.1145\/1644001.1644003"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Delahaye, D.: A Proof Dedicated Meta-Language. In: Pfenning, F. (ed.) Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark). Electronic Notes in Theoretical Computer Science (ENTCS), vol.\u00a070(2), pp. 96\u2013109. Elsevier (2002)","DOI":"10.1016\/S1571-0661(04)80508-5"},{"key":"3_CR22","unstructured":"The Frama-C platform for static analysis of C programs, \n                  \n                    http:\/\/www.frama-c.cea.fr\/"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45842-5_7","volume-title":"Types for Proofs and Programs","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Wiedijk, F., Zwanenburg, J.: A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 96\u2013111. Springer, Heidelberg (2002), \n                  \n                    http:\/\/www.cs.ru.nl\/~freek\/fta\/"},{"issue":"11","key":"3_CR24","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof the four-color theorem. Notices of the AMS\u00a055(11), 1382\u20131393 (2008), \n                  \n                    http:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf","journal-title":"Notices of the AMS"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-22863-6_2","volume-title":"Interactive Theorem Proving","author":"G. Gonthier","year":"2011","unstructured":"Gonthier, G.: Advances in the Formalization of the Odd Order Theorem. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, p. 2. Springer, Heidelberg (2011)"},{"key":"3_CR26","unstructured":"Hales, T.: Flyspeck project. The purpose of the flyspeck project is to produce a formal proof of the Kepler Conjecture, \n                  \n                    http:\/\/code.google.com\/p\/flyspeck\/"},{"key":"3_CR27","unstructured":"Harrison, J.: The HOL Light theorem prover, \n                  \n                    http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J.V. Harrison","year":"1999","unstructured":"Harrison, J.V.: A Machine-Checked Theory of Floating Point Arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 113\u2013130. Springer, Heidelberg (1999)"},{"issue":"7","key":"3_CR29","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052(7), 107\u2013115 (2009), \n                  \n                    http:\/\/compcert.inria.fr\/","journal-title":"Communications of the ACM"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P. Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: An Overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol.\u00a05028, pp. 359\u2013369. Springer, Heidelberg (2008)"},{"key":"3_CR31","unstructured":"McBride, C., et al.: Epigram 2: an experimental dependently typed functional programming language, \n                  \n                    http:\/\/www.e-pig.org\/darcs\/Pig09\/web\/"},{"key":"3_CR32","unstructured":"Morrisett, G., et al.: The Ynot project, \n                  \n                    http:\/\/ynot.cs.harvard.edu\/"},{"key":"3_CR33","unstructured":"Norrish, M., Slind, K., et al.: HOL theorem-proving system (HOL4), \n                  \n                    http:\/\/hol.sourceforge.net\/"},{"key":"3_CR34","unstructured":"University of Pennsylvania & University of Cambridge. The POPLmark challenge (2006), \n                  \n                    https:\/\/alliance.seas.upenn.edu\/~plclub\/cgi-bin\/poplmark\/"},{"key":"3_CR35","unstructured":"Owre, S., Rushby, J., Shankar, N., et al.: PVS specification and verification system, \n                  \n                    http:\/\/pvs.csl.sri.com\/"},{"key":"3_CR36","unstructured":"Paulson, L., Nipkow, T., Wenzel, M.: Isabelle, \n                  \n                    http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle"},{"key":"3_CR37","unstructured":"Pierce, B.C., Casinghino, C., Greenberg, M., Sj\u00f6berg, V., Yorgey, B.: Software Foundations. University of Pennsylvania (2011), \n                  \n                    http:\/\/www.cis.upenn.edu\/~bcpierce\/sf\/"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Sozeau, M.: Programing finger trees in Coq. In: Hinze, R., Ramsey, N. (eds.) Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, pp. 13\u201324. ACM (2007)","DOI":"10.1145\/1291151.1291156"},{"key":"3_CR39","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual \u2013 Version V8.3 (2010), \n                  \n                    http:\/\/coq.inria.fr"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-74591-4_24","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Th\u00e9ry","year":"2007","unstructured":"Th\u00e9ry, L., Hanrot, G.: Primality Proving with Elliptic Curves. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 319\u2013333. Springer, Heidelberg (2007), \n                  \n                    http:\/\/coqprime.gforge.inria.fr\/"}],"container-title":["Lecture Notes in Computer Science","Tools for Practical Software Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35746-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:36:49Z","timestamp":1558301809000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35746-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642357459","9783642357466"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35746-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}