{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:37:06Z","timestamp":1754483826369,"version":"3.40.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319117362"},{"type":"electronic","value":"9783319117379"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11737-9_10","type":"book-chapter","created":{"date-parts":[[2014,10,15]],"date-time":"2014-10-15T00:52:14Z","timestamp":1413334334000},"page":"139-154","source":"Crossref","is-referenced-by-count":1,"title":["Pointer Program Derivation Using Coq: Graphs and Schorr-Waite Algorithm"],"prefix":"10.1007","author":[{"given":"Jean-Fran\u00e7ois","family":"Dufourd","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-45236-2_5","volume-title":"FME 2003: Formal Methods","author":"J.-R. Abrial","year":"2003","unstructured":"Abrial, J.-R.: Event Based Sequential Program Development: Application to Constructing a Pointer Program. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 51\u201374. Springer, Heidelberg (2003)"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Springer-Verlag (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R. Bornat","year":"2000","unstructured":"Bornat, R.: Proving Pointer Programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 102\u2013126. Springer, Heidelberg (2000)"},{"issue":"3","key":"10_CR4","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/357172.357175","volume":"4","author":"M. Broy","year":"1982","unstructured":"Broy, M., Pepper, P.: Combining Algebraic and Algorithmic Reasoning: An Approach to the Schorr-Waite Algorithm. ACM-TOPLAS\u00a04(3), 362\u2013381 (1982)","journal-title":"ACM-TOPLAS"},{"key":"10_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/978-3-540-69061-0_15","volume-title":"Verification of Object-Oriented Software. The KeY Approach","author":"R. Bubel","year":"2007","unstructured":"Bubel, R.: The schorr-waite-algorithm. In: Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.) Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334, pp. 569\u2013587. Springer, Heidelberg (2007)"},{"key":"10_CR6","first-page":"23","volume":"7","author":"R.M. Burstall","year":"1972","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alters data structures. Machine Intelligence\u00a07, 23\u201350 (1972)","journal-title":"Machine Intelligence"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI, pp. 234\u2013245 (2011)","DOI":"10.1145\/1993316.1993526"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/3-540-08342-1_32","volume-title":"Automata, Languages and Programming","author":"W.-P. Roever de","year":"1977","unstructured":"de Roever, W.-P.: On Backtracking and Greatest Fixpoints. In: Salomaa, A., Steinby, M. (eds.) ICALP 1977. LNCS, vol.\u00a052, pp. 412\u2013429. Springer, Heidelberg (1977)"},{"issue":"3","key":"10_CR9","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(80)90130-1","volume":"11","author":"N. Dershowitz","year":"1980","unstructured":"Dershowitz, N.: The Schorr-Waite Marking Algorithm Revisited. Inf. Proc. Lett.\u00a011(3), 141\u2013143 (1980)","journal-title":"Inf. Proc. Lett."},{"issue":"2-3","key":"10_CR10","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/j.tcs.2008.02.012","volume":"403","author":"J.-F. Dufourd","year":"2008","unstructured":"Dufourd, J.-F.: Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof. Theor. Comp. Sci.\u00a0403(2-3), 133\u2013159 (2008)","journal-title":"Theor. Comp. Sci."},{"key":"10_CR11","unstructured":"Dufourd, J.-F.: D\u00e9rivation de l\u2019algorithme de Schorr-Waite en Coq par une m\u00e9thode alg\u00e9brique. In: JFLA 2012, INRIA (2012), http:\/\/hal.inria.fr\/hal-00665909"},{"key":"10_CR12","unstructured":"Dufourd, J.-F.: Schorr-Waite Coq Development On-line Documentation (2013), http:\/\/dpt-info.u-strasbg.fr\/~jfd\/SW-LIB-PUBLI.tar.gz"},{"key":"10_CR13","unstructured":"Dufourd, J.-F.: Formal Study of Functional Orbits in Finite Domains, 35 pages (2013) (submitted)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-319-08970-6_16","volume-title":"Interactive Theorem Proving","author":"J.-F. Dufourd","year":"2014","unstructured":"Dufourd, J.-F.: Hypermap specification and certified linked implementation using orbits. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol.\u00a08558, pp. 242\u2013257. Springer, Heidelberg (2014)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-20551-4_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. Giorgino","year":"2011","unstructured":"Giorgino, M., Strecker, M., Matthes, R., Pantel, M.: Verification of the schorr-waite algorithm \u2013 from trees to graphs. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol.\u00a06564, pp. 67\u201383. Springer, Heidelberg (2011)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-27705-4_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"J.-C. Filli\u00e2tre","year":"2012","unstructured":"Filli\u00e2tre, J.-C.: Verifying two lines of C with why3: An exercise in program verification. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 83\u201397. Springer, Heidelberg (2012)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/BFb0014678","volume-title":"Program Construction","author":"S.L. Gerhardt","year":"1979","unstructured":"Gerhardt, S.L.: A derivation-oriented proof of the Schorr-Waite algorithm. In: Gerhart, S.L., et al. (eds.) Program Construction. LNCS, vol.\u00a069, pp. 472\u2013492. Springer, Heidelberg (1979)"},{"issue":"11","key":"10_CR18","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)","journal-title":"Notices of the AMS"},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00289068","volume":"11","author":"D. Gries","year":"1979","unstructured":"Gries, D.: The Schorr-Waite Graph Marking Algorithm. Acta Informatica\u00a011, 223\u2013232 (1979)","journal-title":"Acta Informatica"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/BFb0014677","volume-title":"Program Construction","author":"M. Griffiths","year":"1979","unstructured":"Griffiths, M.: Development of the Schorr-Waite algorithm. In: Gerhart, S.L., Pair, C., Pepper, P.A., W\u00f6ssner, H., Dijkstra, E.W., Guttag, J.V., Owicki, S.S., Partsch, H., Bauer, F.L., Gries, D., Griffiths, M., Horning, J.J., Wirsing, M. (eds.) Program Construction. LNCS, vol.\u00a069, pp. 464\u2013471. Springer, Heidelberg (1979)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Hackett, B., Rugina, R.: Region-Based Shape Analysis with Tracked Locations. In: 32nd ACM POPL 2005, pp. 310\u2013323 (2005)","DOI":"10.1145\/1047659.1040331"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Hubert, T., March\u00e9, C.: A case study of C source code verification; the Schorr-Waite algorithm. In: 3rd IEEE SEFM 2005, pp. 190\u2013199 (2005)","DOI":"10.1109\/SEFM.2005.1"},{"key":"10_CR23","unstructured":"Knuth, D.E.: The Art of Computer Programming: Fundamental Algorithms, vol.\u00a0I. Add. -Wesley (1968)"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"issue":"1","key":"10_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X. Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. JAR\u00a041(1), 1\u201331 (2008)","journal-title":"JAR"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/11823230_17","volume-title":"Static Analysis","author":"A. Loginov","year":"2006","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Automated verification of the deutsch-schorr-waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 261\u2013279. Springer, Heidelberg (2006)"},{"issue":"1-2","key":"10_CR27","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F. Mehta","year":"2005","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Info. and Comp.\u00a0199(1-2), 200\u2013227 (2005)","journal-title":"Info. and Comp."},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Morris, J.M.: A Proof of the Schorr-Waite Algorithm. In: TFPM, vol.\u00a091, pp. 43\u201351. NATO, D. Reidel (1982)","DOI":"10.1007\/978-94-009-7893-5_5"},{"issue":"1","key":"10_CR29","first-page":"67","volume":"24","author":"V. Preoteasa","year":"2012","unstructured":"Preoteasa, V., Back, R.-J.: Invariant diagrams with data refinement. FAC\u00a024(1), 67\u201395 (2012)","journal-title":"FAC"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"8","key":"10_CR31","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/363534.363554","volume":"10","author":"H. Schorr","year":"1967","unstructured":"Schorr, H., Waite, W.R.: An Efficient Machine-Independent Procedure for Garbage Collection in Various List Structures. CACM\u00a010(8), 501\u2013506 (1967)","journal-title":"CACM"},{"key":"10_CR32","unstructured":"Suzuki, N.: Automatic Verification of Programs with Complex Data Structures. PhD Th., Dept. of CS, Stanford (1976)"},{"key":"10_CR33","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/BF00289067","volume":"11","author":"R.W. Topor","year":"1979","unstructured":"Topor, R.W.: The Correctness of the Schorr-Waite List Marking Algorithm. Acta Inf.\u00a011, 211\u2013221 (1979)","journal-title":"Acta Inf."},{"issue":"9","key":"10_CR34","first-page":"665","volume":"22","author":"M. Ward","year":"1996","unstructured":"Ward, M.: Derivation of Data Intensive Algorithms by Formal Transformation. IEEE-TOSE\u00a022(9), 665\u2013686 (1996)","journal-title":"IEEE-TOSE"},{"issue":"1-3","key":"10_CR35","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1016\/j.tcs.2006.12.036","volume":"375","author":"H. Yang","year":"2007","unstructured":"Yang, H.: Relational separation logic. TCS\u00a0375(1-3), 308\u2013334 (2007)","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11737-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T04:24:54Z","timestamp":1746419094000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11737-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319117362","9783319117379"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11737-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}