{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:58:02Z","timestamp":1742918282118,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642253782"},{"type":"electronic","value":"9783642253799"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-25379-9_5","type":"book-chapter","created":{"date-parts":[[2011,11,13]],"date-time":"2011-11-13T20:33:47Z","timestamp":1321216427000},"page":"37-53","source":"Crossref","is-referenced-by-count":2,"title":["Automated Certification of Implicit Induction Proofs"],"prefix":"10.1007","author":[{"given":"Sorin","family":"Stratulat","sequence":"first","affiliation":[]},{"given":"Vincent","family":"Demange","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"5_CR1","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1006\/jsco.2002.0549","volume":"34","author":"A. Armando","year":"2002","unstructured":"Armando, A., Rusinowitch, M., Stratulat, S.: Incorporating decision procedures in implicit induction. J. Symb. Comput.\u00a034(4), 241\u2013258 (2002)","journal-title":"J. Symb. Comput."},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44881-0_24","volume-title":"Rewriting Techniques and Applications","author":"G. Barthe","year":"2003","unstructured":"Barthe, G., Stratulat, S.: Validation of the JavaCard Platform with Implicit Induction Techniques. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 337\u2013351. Springer, Heidelberg (2003)"},{"key":"5_CR4","unstructured":"Berger, A., Bonomi, F., Fendick, K.: Proposed TM baseline text on an ABR conformance definition. Technical Report 95-0212R1, ATM Forum Traffic Management Group (1995)"},{"issue":"5","key":"5_CR5","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1093\/logcom\/5.5.631","volume":"5","author":"A. Bouhoula","year":"1995","unstructured":"Bouhoula, A., Kounalis, E., Rusinowitch, M.: Automated mathematical induction. Journal of Logic and Computation\u00a05(5), 631\u2013668 (1995)","journal-title":"Journal of Logic and Computation"},{"key":"5_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-74621-8_10","volume-title":"Frontiers of Combining Systems","author":"E. Contejean","year":"2007","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Certification of Automated Termination Proofs. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 148\u2013162. Springer, Heidelberg (2007)"},{"key":"#cr-split#-5_CR7.1","unstructured":"Courant, J.: Proof reconstruction. Research Report RR96-26, LIP (1996);"},{"key":"#cr-split#-5_CR7.2","unstructured":"Preliminary version"},{"key":"5_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A Tactic Language for the System Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 85\u201395. Springer, Heidelberg (2000)"},{"key":"5_CR9","unstructured":"ITU-T. Traffic control and congestion control in B ISDN. Recommandation I.371.1 (1997)"},{"key":"5_CR10","unstructured":"Kaliszyk, C.: Validation des preuves par r\u00e9currence implicite avec des outils bas\u00e9s sur le calcul des constructions inductives. Master\u2019s thesis, Universit\u00e9 Paul Verlaine - Metz (2005)"},{"issue":"6","key":"5_CR11","doi-asserted-by":"publisher","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. Communications of the ACM\u00a053(6), 107\u2013115 (2010)","journal-title":"Communications of the ACM"},{"key":"5_CR12","unstructured":"Leroy, X., Doligez, D., Frisch, A., Garrigue, J., R\u00e9my, D., Vouillon, J.: The Objective Caml system - release 3.12. Documentation and user\u2019s manual. INRIA"},{"issue":"1\u20132","key":"5_CR13","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10472-009-9154-5","volume":"55","author":"F. Nahon","year":"2009","unstructured":"Nahon, F., Kirchner, C., Kirchner, H., Brauner, P.: Inductive proof search modulo. Annals of Mathematics and Artificial Intelligence\u00a055(1\u20132), 123\u2013154 (2009)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"5_CR14","unstructured":"Rabadan, C., Klay, F.: Un nouvel algorithme de contr\u00f4le de conformit\u00e9 pour la capacit\u00e9 de transfert \u2018Available Bit Rate\u2019. Technical Report NT\/CNET\/5476, CNET (1997)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Rusinowitch, M., Stratulat, S., Klay, F.: Mechanical verification of a generic incremental ABR conformance algorithm. Technical Report 3794, INRIA (1999)","DOI":"10.1007\/10722167_27"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/10722167_27","volume-title":"Computer Aided Verification","author":"M. Rusinowitch","year":"2000","unstructured":"Rusinowitch, M., Stratulat, S., Klay, F.: Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 344\u2013357. Springer, Heidelberg (2000)"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1023\/A:1023251327012","volume":"30","author":"M. Rusinowitch","year":"2003","unstructured":"Rusinowitch, M., Stratulat, S., Klay, F.: Mechanical verification of an ideal incremental ABR conformance algorithm. J. Autom. Reasoning\u00a030(2), 53\u2013177 (2003)","journal-title":"J. Autom. Reasoning"},{"key":"5_CR18","unstructured":"Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS prover guide - version 2.4. SRI International (November 2001)"},{"issue":"4","key":"5_CR19","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1006\/jsco.2000.0469","volume":"32","author":"S. Stratulat","year":"2001","unstructured":"Stratulat, S.: A general framework to build contextual cover set induction provers. J. Symb. Comput.\u00a032(4), 403\u2013445 (2001)","journal-title":"J. Symb. Comput."},{"key":"5_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11554554_20","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Stratulat","year":"2005","unstructured":"Stratulat, S.: Automatic \u2018Descente Infinie\u2019 Induction Reasoning. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 262\u2013276. Springer, Heidelberg (2005)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Stratulat, S.: \u2018Descente Infinie\u2019 induction-based saturation procedures. In: SYNASC 2007: Proceedings of the Ninth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Washington, DC, USA, pp. 17\u201324. IEEE Computer Society (2007)","DOI":"10.1109\/SYNASC.2007.17"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-540-70590-1_24","volume-title":"Rewriting Techniques and Applications","author":"S. Stratulat","year":"2008","unstructured":"Stratulat, S.: Combining Rewriting with Noetherian Induction to Reason on Non-Orientable Equalities. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol.\u00a05117, pp. 351\u2013365. Springer, Heidelberg (2008)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-642-16265-7_23","volume-title":"Integrated Formal Methods","author":"S. Stratulat","year":"2010","unstructured":"Stratulat, S.: Integrating Implicit Induction Proofs into Certified Proof Environments. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol.\u00a06396, pp. 320\u2013335. Springer, Heidelberg (2010)"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Stratulat, S., Demange, V.: Validating implicit induction proofs using certified proof environments. In: Poster Session of 2010 Grande Region Security and Reliability Day, Saarbrucken (March 2010)","DOI":"10.1007\/978-3-642-16265-7_23"},{"key":"5_CR25","unstructured":"The Coq\u00a0Development Team. The Coq reference manual - version 8.2 (2009), http:\/\/coq.inria.fr\/doc"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25379-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T09:39:21Z","timestamp":1560937161000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25379-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642253782","9783642253799"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25379-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}