{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T09:04:04Z","timestamp":1743498244317},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642156502"},{"type":"electronic","value":"9783642156519"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15651-9_26","type":"book-chapter","created":{"date-parts":[[2010,8,10]],"date-time":"2010-08-10T09:12:19Z","timestamp":1281431539000},"page":"347-360","source":"Crossref","is-referenced-by-count":20,"title":["Experiences in Applying Formal Verification in Robotics"],"prefix":"10.1007","author":[{"given":"Dennis","family":"Walter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"T\u00e4ubig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","volume-title":"ISSSE 2006","author":"J. Barnes","year":"2006","unstructured":"Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the tokeneer enclave protection software. In: ISSSE 2006, IEEE Computer Society, Los Alamitos (2006)"},{"key":"26_CR2","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI C specification language (October 2008), Version 1.4, \n                      \n                        http:\/\/frama-c.cea.fr\/download\/acsl_1.4.pdf"},{"key":"26_CR3","volume-title":"ARITH18","author":"S. Boldo","year":"2007","unstructured":"Boldo, S., Filli\u00e2tre, J.-C.: Formal verification of floating-point programs. In: ARITH18, Montpellier, France, June 2007, IEEE Computer Society, Los Alamitos (2007)"},{"issue":"3","key":"26_CR4","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. STTT\u00a07(3), 212\u2013232 (2005)","journal-title":"Int. J. STTT"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"26_CR6","series-title":"ENTCS","volume-title":"SafeCert 2008","author":"U. Frese","year":"2008","unstructured":"Frese, U., Hausmann, D., L\u00fcth, C., T\u00e4ubig, H., Walter, D.: The importance of being formal. In: SafeCert 2008. ENTCS, Elsevier Science, Amsterdam (2008)"},{"issue":"11-12","key":"26_CR7","doi-asserted-by":"publisher","first-page":"1507","DOI":"10.1177\/0278364909343970","volume":"28","author":"S. Haddadin","year":"2009","unstructured":"Haddadin, S., Albu-Schaffer, A., Hirzinger, G.: Requirements for safe robots: Measurements, analysis and new insights. Int. J. Robot. Res.\u00a028(11-12), 1507\u20131527 (2009)","journal-title":"Int. J. Robot. Res."},{"key":"26_CR8","first-page":"265","volume-title":"RE 2007","author":"C. Heitmeyer","year":"2007","unstructured":"Heitmeyer, C., Jeffords, R., Bharadwaj, R., Archer, M.: RE theory meets software practice: Lessons from the software development trenches. In: RE 2007, pp. 265\u2013268. IEEE Computer Society, Los Alamitos (2007)"},{"issue":"10","key":"26_CR9","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/1562764.1562779","volume":"52","author":"C. Hoare","year":"2009","unstructured":"Hoare, C.: Viewpoint retrospective: an axiomatic basis for computer programming. Commun. ACM\u00a052(10), 30\u201332 (2009)","journal-title":"Commun. ACM"},{"key":"26_CR10","unstructured":"IEC. IEC\u00a061508 \u2013 Functional safety of electrical\/ electronic\/ programmable electronic safety-related systems. IEC, Geneva, Switzerland (2000)"},{"issue":"3","key":"26_CR11","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1016\/j.robot.2005.10.008","volume":"54","author":"K.M. Krishna","year":"2006","unstructured":"Krishna, K.M., Alami, R., Simeon, T.: Safe proactive plans and their execution. Robot. Auton. Syst.\u00a054(3), 244\u2013255 (2006)","journal-title":"Robot. Auton. Syst."},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-642-05089-3_27","volume-title":"FM 2009: Formal Methods","author":"C. L\u00fcth","year":"2009","unstructured":"L\u00fcth, C., Walter, D.: Certifiable specification and verification of C programs. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 419\u2013434. Springer, Heidelberg (2009)"},{"key":"26_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11615798_1","volume-title":"Automated Deduction in Geometry","author":"L.I. Meikle","year":"2006","unstructured":"Meikle, L.I., Fleuriot, J.D.: Mechanical theorem proving in computational geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol.\u00a03763, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-85762-4_2","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"J. Peleska","year":"2008","unstructured":"Peleska, J.: A unified approach to abstract interpretation, formal verification and testing of C\/C++ modules. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol.\u00a05160, pp. 3\u201322. Springer, Heidelberg (2008)"},{"issue":"2-4","key":"26_CR16","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s10817-009-9120-2","volume":"42","author":"H. Tuch","year":"2009","unstructured":"Tuch, H.: Formal verification of C systems code. J. Autom. Reasoning\u00a042(2-4), 125\u2013187 (2009)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15651-9_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T13:00:22Z","timestamp":1619787622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15651-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642156502","9783642156519"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15651-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}