{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:17:04Z","timestamp":1743149824133,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642386121"},{"type":"electronic","value":"9783642386138"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38613-8_9","type":"book-chapter","created":{"date-parts":[[2013,5,13]],"date-time":"2013-05-13T02:45:19Z","timestamp":1368413119000},"page":"124-138","source":"Crossref","is-referenced-by-count":7,"title":["Deductive Verification of State-Space Algorithms"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Gava","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean","family":"Fortin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Guedj","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","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":"9_CR2","unstructured":"Barnat, J.: Distributed Memory LTL Model Checking. PhD thesis, Faculty of Informatics Masaryk University Brno (2004)"},{"key":"9_CR3","unstructured":"Barras, B., Werner, B.: Coq in Coq. Technical report, INRIA (1997)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Bisseling, R.H.: Parallel scientific computation. A structured approach using BSP and MPI. Oxford University Press (2004)","DOI":"10.1093\/acprof:oso\/9780198529392.001.0001"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 179\u2013194. Springer, Heidelberg (2010)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Computer Aided Verification, CAV (to appear, 2013)","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"9_CR7","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":"9_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45620-1_29","volume-title":"Automated Deduction - CADE-18","author":"J. Ford","year":"2002","unstructured":"Ford, J., Shankar, N.: Formal verification of a combination decision procedure. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 347\u2013362. Springer, Heidelberg (2002)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Fortin, J., Gava, F.: BSP-WHY: an intermediate language for deductive verification of BSP programs. In: High-Level Parallel Programming and Applications (HLPP), pp. 35\u201344. ACM (2010)","DOI":"10.1145\/1863482.1863491"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-642-25318-8_24","volume-title":"Programming Languages and Systems","author":"L. Fronc","year":"2011","unstructured":"Fronc, L., Pommereau, F.: Towards a certified Petri net model-checker. In: Yang, H. (ed.) APLAS 2011. LNCS, vol.\u00a07078, pp. 322\u2013336. Springer, Heidelberg (2011)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-45139-0_14","volume-title":"Model Checking Software","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.M.: Parallel state space construction for model-checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 217\u2013234. Springer, Heidelberg (2001)"},{"key":"9_CR12","unstructured":"Herms, P.: Certification of a chain for deductive program verification. In: Bertot, Y. (ed.) 2nd Coq Workshop, Satellite of ITP 2010 (2010)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 2\u201313. Springer, Heidelberg (2001)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages (POPL), pp. 106\u2013119. ACM (1997)","DOI":"10.1145\/263699.263712"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-45294-X_25","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"D. Peled","year":"2001","unstructured":"Peled, D., Pnueli, A., Zuck, L.D.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 292\u2013304. Springer, Heidelberg (2001)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/3-540-44755-5_25","volume-title":"Theorem Proving in Higher Order Logics","author":"X. Rival","year":"2001","unstructured":"Rival, X., Goubault-Larrecq, J.: Experiments with finite tree automata in Coq. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 362\u2013377. Springer, Heidelberg (2001)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-03359-9_29","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Schimpf","year":"2009","unstructured":"Schimpf, A., Merz, S., Smaus, J.-G.: Construction of B\u00fcchi Automata for LTL Model Checking Verified in Isabelle\/HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 424\u2013439. Springer, Heidelberg (2009)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-88387-6_3","volume-title":"Automated Technology for Verification and Analysis","author":"N. Shankar","year":"2008","unstructured":"Shankar, N.: Trust and automation in verification tools. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 4\u201317. Springer, Heidelberg (2008)"},{"issue":"3","key":"9_CR19","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1155\/1997\/532130","volume":"6","author":"D.B. Skillicorn","year":"1997","unstructured":"Skillicorn, D.B., Hill, J.M.D., McColl, W.F.: Questions and answers about BSP. Scientific Programming\u00a06(3), 249\u2013274 (1997)","journal-title":"Scientific Programming"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0054171","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Sprenger","year":"1998","unstructured":"Sprenger, C.: A verified model checker for the modal \u03bc-calculus in coq. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 167\u2013183. Springer, Heidelberg (1998)"},{"issue":"1","key":"9_CR21","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10703-012-0163-3","volume":"42","author":"A. Stump","year":"2013","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Methods in System Design\u00a042(1), 91\u2013118 (2013)","journal-title":"Formal Methods in System Design"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-642-16901-4_34","volume-title":"Formal Methods and Software Engineering","author":"J. Sun","year":"2010","unstructured":"Sun, J., Liu, Y., Cheng, B.: Model checking a model checker: A code contract combined approach. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 518\u2013533. Springer, Heidelberg (2010)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-45657-0_37","volume-title":"Computer Aided Verification","author":"L. Tan","year":"2002","unstructured":"Tan, L., Cleaveland, W.R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 455\u2013470. Springer, Heidelberg (2002)"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-77505-8_25","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"M.-H. Tsai","year":"2008","unstructured":"Tsai, M.-H., Wang, B.-Y.: Formalization of cTL* in calculus of inductive constructions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 316\u2013330. Springer, Heidelberg (2008)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-11811-1_18","volume-title":"Abstract State Machines, Alloy, B and Z","author":"E. Turner","year":"2010","unstructured":"Turner, E., Butler, M., Leuschel, M.: A refinement-based correctness proof of symmetry reduced model checking. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 231\u2013244. Springer, Heidelberg (2010)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-44464-5_13","volume-title":"Advances in Computing Science - ASIAN 2000","author":"K.N. Verma","year":"2000","unstructured":"Verma, K.N., Goubault-Larrecq, J., Prasad, S., Arun-Kumar, S.: Reflecting BDDs in Coq. In: Kleinberg, R.D., Sato, M. (eds.) ASIAN 2000. LNCS, vol.\u00a01961, pp. 162\u2013181. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38613-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T11:47:39Z","timestamp":1676807259000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-38613-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642386121","9783642386138"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38613-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}