{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T04:06:30Z","timestamp":1751688390712,"version":"3.41.0"},"publisher-location":"Cham","reference-count":8,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319912707"},{"type":"electronic","value":"9783319912714"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-91271-4_33","type":"book-chapter","created":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T14:32:55Z","timestamp":1525703575000},"page":"415-419","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Teaching an Old Dog New Tricks"],"prefix":"10.1007","author":[{"given":"Lilian","family":"Burdy","sequence":"first","affiliation":[]},{"given":"David","family":"Deharbe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,8]]},"reference":[{"key":"33_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. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017)","key":"33_CR2"},{"unstructured":"CENELEC - EN 50128: Railway applications-communication, signaling and processing systems-software for railway control and protection systems (2011)","key":"33_CR3"},{"key":"33_CR4","first-page":"207","volume":"9","author":"DR Cok","year":"2016","unstructured":"Cok, D.R., D\u00e9harbe, D., Weber, T.: The 2014 SMT competition. J. Satisf. Boolean Model. Comput. 9, 207\u2013242 (2016)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"2","key":"33_CR5","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1590\/S0104-65002003000300003","volume":"9","author":"J Couchot","year":"2004","unstructured":"Couchot, J., D\u00e9harbe, D., Giorgetti, A., Ranise, S.: Scalable automated proving and debugging of set-based specifications. J. Braz. Comput. Soc. 9(2), 17\u201336 (2004)","journal-title":"J. Braz. Comput. Soc."},{"key":"33_CR6","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1016\/j.scico.2014.04.012","volume":"94","author":"D D\u00e9harbe","year":"2014","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in Rodin. Sci. Comput. Program. 94, 130\u2013143 (2014)","journal-title":"Sci. Comput. Program."},{"key":"33_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer Science & Business Media, Berlin (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: PAAR@ IJCAR, pp. 1\u201310 (2010)","key":"33_CR8","DOI":"10.29007\/tnfd"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91271-4_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T08:42:39Z","timestamp":1751618559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91271-4_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319912707","9783319912714"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91271-4_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}