{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T18:45:03Z","timestamp":1770835503409,"version":"3.50.1"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2014,4,19]],"date-time":"2014-04-19T00:00:00Z","timestamp":1397865600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1007\/s10009-014-0314-5","type":"journal-article","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T18:26:33Z","timestamp":1397845593000},"page":"709-727","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":41,"title":["Let\u2019s verify this with Why3"],"prefix":"10.1007","volume":"17","author":[{"given":"Fran\u00e7ois","family":"Bobot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Paskevich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,4,19]]},"reference":[{"key":"314_CR1","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd international conference on Computer aided verification, CAV\u201911, pp. 171\u2013177. Heidelberg, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"314_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) 19th International Conference on Computer Aided Verification, vol 4590 of Lecture Notes in Computer Science, pp. 298\u2013302. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"314_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer-Verlag, Berlin (2004)"},{"key":"314_CR4","unstructured":"Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover. (2008) http:\/\/alt-ergo.lri.fr\/"},{"key":"314_CR5","doi-asserted-by":"crossref","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Melquiond, G., Paskevich, A.: Preserving user proofs across specification changes. In: Cohen, E., Rybalchenko, A. (eds.) Verified software: theories, tools, experiments (5th International Conference VSTTE), vol 8164 of Lecture Notes in Computer Science, pp. 191\u2013201. Springer, Atherton (2013)","DOI":"10.1007\/978-3-642-54108-7_10"},{"key":"314_CR6","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Melquiond, G., Paskevich, A.: The Why3 platform, version 0.82. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.82 edition. (2013) http:\/\/why3.lri.fr\/download\/manual-0.82.pdf"},{"key":"314_CR7","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie (ed.) First International Workshop on Intermediate Verification Languages, pp. 53\u201364. Wroc\u0142aw, Poland (2011)"},{"key":"314_CR8","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3, an efficient SMT solver. In: TACAS, vol 4963 of Lecture Notes in Computer Science, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"314_CR9","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Proceedings of the 22nd European Symposium on Programming, vol 7792 of Lecture Notes in Computer Science, pp. 125\u2013128. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"314_CR10","unstructured":"The Frama-C platform for static analysis of C programs. (2008) http:\/\/www.frama-c.cea.fr\/"},{"issue":"5","key":"314_CR11","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"G Huet","year":"1997","unstructured":"Huet, G.: The Zipper. J. Fun. Progr. 7(5), 549\u2013554 (1997)","journal-title":"J. Fun. Progr."},{"key":"314_CR12","unstructured":"Leino, K.R.M., Moskal, M.: VACID-0: Verification of ample correctness of invariants of data-structures. In: Proceedings of Tools and Experiments Workshop at VSTTE (2010)"},{"key":"314_CR13","unstructured":"March\u00e9, C.: The Krakatoa tool for deductive verification of Java programs. Winter school on object-oriented verification, Viinistu, Estonia. (2009) http:\/\/krakatoa.lri.fr\/ws\/"},{"key":"314_CR14","unstructured":"Moy, Y., March\u00e9, C.: The Jessie plugin for deduction verification in Frama-C \u2013 tutorial and reference manual. INRIA & LRI. (2011) http:\/\/krakatoa.lri.fr\/"},{"key":"314_CR15","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed). 11th International Conference on Automated Deduction, vol 607 of Lecture Notes in Computer Science, pp. 748\u2013752. Springer, Saratoga Springs (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"314_CR16","doi-asserted-by":"crossref","unstructured":"Riazanov, A., Voronkov, A.: Vampire. In: Ganzinger, H. (ed.) 16th International Conference on Automated Deduction, vol 1632 of Lecture Notes in Artificial Intelligence, pp. 292\u2013296. Springer, Trento (1999)","DOI":"10.1007\/3-540-48660-7_26"},{"key":"314_CR17","doi-asserted-by":"crossref","unstructured":"Schulz, S.: System description: E 0.81. In: Basin, D.A., Rusinowitch, M. (eds) Second International Joint Conference on Automated Reasoning, vol 3097 of Lecture Notes in Computer Science, pp. 223\u2013228. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-25984-8_15"},{"key":"314_CR18","doi-asserted-by":"crossref","unstructured":"Summers, A.J., Mueller, P.: Freedom before commitment: a lightweight type system for object initialisation. In: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications, OOPSLA \u201911, pp. 1013\u20131032. ACM, New York (2011)","DOI":"10.1145\/2048066.2048142"},{"key":"314_CR19","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) 22nd International Conference on Automated Deduction, vol 5663 of Lecture Notes in Computer Science, pp 140\u2013145. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02959-2_10"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0314-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0314-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0314-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T13:47:51Z","timestamp":1565358471000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0314-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,19]]},"references-count":19,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["314"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0314-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,19]]}}}