{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T04:32:42Z","timestamp":1725769962304},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642541070"},{"type":"electronic","value":"9783642541087"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54108-7_10","type":"book-chapter","created":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T05:09:36Z","timestamp":1389762576000},"page":"191-201","source":"Crossref","is-referenced-by-count":12,"title":["Preserving User Proofs across Specification Changes"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Bobot","sequence":"first","affiliation":[]},{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"additional","affiliation":[]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Paskevich","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"10_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"10_CR3","unstructured":"Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover (2008), \n                  \n                    http:\/\/alt-ergo.lri.fr\/"},{"key":"10_CR4","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, pp. 53\u201364 (August 2011)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-24364-6_7","volume-title":"Frontiers of Combining Systems","author":"F. Bobot","year":"2011","unstructured":"Bobot, F., Paskevich, A.: Expressing Polymorphic Types in a Many-Sorted Language. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol.\u00a06989, pp. 87\u2013102. Springer, Heidelberg (2011)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-35873-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Cruanes","year":"2013","unstructured":"Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the evidential tool bus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 275\u2013294. Springer, Heidelberg (2013)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"10_CR8","unstructured":"Filli\u00e2tre, J.-C.: Combining Interactive and Automated Theorem Proving in Why3 (invited talk). In: Heljanko, K., Herbelin, H. (eds.) Automation in Proof Assistants 2012, Tallinn, Estonia (April 2012)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J.-C. Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. LNCS, vol.\u00a07792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"key":"10_CR10","unstructured":"Klebanov, V.: Extending the Reach and Power of Deductive Program Verification. PhD thesis, Universit\u00e4t Koblenz-Landau (2009), \n                  \n                    http:\/\/formal.iti.kit.edu\/~klebanov\/pubs\/vstte09.pdf"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Miller, D., Pimentel, E.: A formal framework for specifying sequent calculus proof systems. In: Theoretical Computer Science, pp. 98\u2013116 (2013)","DOI":"10.1016\/j.tcs.2012.12.008"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-57529-4_61","volume-title":"Foundations of Software Technology and Theoretical Computer Science, 13th Conference","author":"W. Reif","year":"1993","unstructured":"Reif, W., Stenzel, K.: Reuse of proofs in software verification. In: Shyamasundar, R.K. (ed.) FSTTCS 1993. LNCS, vol.\u00a0761, pp. 284\u2013293. Springer, Heidelberg (1993)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11576280_3","volume-title":"Formal Methods and Software Engineering","author":"J. Rushby","year":"2005","unstructured":"Rushby, J.: An evidential tool bus. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, p. 36. Springer, Heidelberg (2005)"},{"key":"10_CR14","unstructured":"Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, vol.\u00a0418. CEUR Workshop Proceedings, pp. 38\u201349 (2008)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54108-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T23:03:56Z","timestamp":1558825436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54108-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642541070","9783642541087"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54108-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}