{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T14:17:24Z","timestamp":1742998644200,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142604"},{"type":"electronic","value":"9783642142611"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-14261-1_15","type":"book-chapter","created":{"date-parts":[[2011,2,8]],"date-time":"2011-02-08T18:07:42Z","timestamp":1297188462000},"page":"145-153","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Specification and Automated Verification of Safety-Critical Requirements of a Railway Vehicle with Frama-C\/Jessie"],"prefix":"10.1007","author":[{"given":"Kerstin","family":"Hartig","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens","family":"Gerlach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan","family":"Soto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Busse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,1,31]]},"reference":[{"key":"15_CR1","unstructured":"CEA LIST, Laboratory of Applied Research on Software-Intensive Technologies, http:\/\/www-list.cea.fr\/gb\/index_gb.htm"},{"key":"15_CR2","unstructured":"March\u00e9, C., Moy, Y.: Jessie Plugin Tutorial, Boron Version, http:\/\/frama-c.com\/jessie\/jessie-tutorial.pdf, (2010)"},{"key":"15_CR3","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, Version 1.4, http:\/\/framac.cea.fr\/download\/acsl_1.4.pdf, (2009)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Souyris, J., Favre-Felix, D.: Proof of properties in avionics, IFIP Congress Topical Sessions, pages 527-536, (2004)","DOI":"10.1007\/978-1-4020-8157-6_48"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Jim Woodcock, et al.: Formal Methods: Practice and Experience, ACM Computing Surveys, Volume 41, Issue 4 (October 2009)","DOI":"10.1145\/1592434.1592436"},{"key":"15_CR6","unstructured":"Burghardt, J., Gerlach, J., Hartig, K., Soto, J., Weber, C.: ACSL By Example, Towards a Verified C Standard Library, http:\/\/www.first.fraunhofer.de\/owx_download\/acsl-by-example-5_1_0.pdf, (2010)"},{"key":"15_CR7","unstructured":"Correnson, L., Cuoq, P., Puccetti, A., Signoles, J.: Frama-C User Manual, Boron Release, http:\/\/frama-c.com\/download\/user-manual-Boron-20100401.pdf, (2010)"},{"key":"15_CR8","unstructured":"Alt-Ergo Theorem Prover, http:\/\/alt-ergo.lri.fr\/."},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3, In Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907), Volume 4590 of Lecture Notes in Computer Science, pages 298-302, (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"15_CR10","unstructured":"Simplify Theorem Prover, http:\/\/secure.ucd.ie\/products\/opensource\/Simplify\/."},{"key":"15_CR11","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT Solver, http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver, Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary, http:\/\/research.microsoft.com\/projects\/z3\/z3.pdf, (2008)","DOI":"10.1007\/978-3-540-78800-3_24"}],"container-title":["FORMS\/FORMAT 2010"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14261-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T20:56:08Z","timestamp":1675198568000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-14261-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642142604","9783642142611"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14261-1_15","relation":{},"subject":[],"published":{"date-parts":[[2011]]},"assertion":[{"value":"31 January 2011","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}