{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:39:36Z","timestamp":1725586776040},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214363"},{"type":"electronic","value":"9783642214370"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_5","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T07:33:16Z","timestamp":1308382396000},"page":"27-41","source":"Crossref","is-referenced-by-count":1,"title":["System Verification through Program Verification"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Dietsch","sequence":"first","affiliation":[]},{"given":"Bernd","family":"Westphal","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10692867_1","volume-title":"Requirements Targeting Software and Systems Engineering","author":"D. Bj\u00f8rner","year":"1998","unstructured":"Bj\u00f8rner, D.: Domains as a prerequisite for requirements and software domain perspectives and facets, requirements aspects and software views. In: Broy, M., Rumpe, B. (eds.) RTSE 1997. LNCS, vol.\u00a01526, pp. 1\u201341. Springer, Heidelberg (1998)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44411-4_1","volume-title":"SOFSEM 2000: Theory and Practice of Informatics","author":"D. Bj\u00f8rner","year":"2000","unstructured":"Bj\u00f8rner, D.: Domain engineering: A software engineering discipline in need of research. In: Hlav\u00e1c, V., Jeffery, K.G., Wiedermann, J. (eds.) SOFSEM 2000. LNCS, vol.\u00a01963, pp. 1\u201317. Springer, Heidelberg (2000)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-39910-0_5","volume-title":"Verification: Theory and Practice","author":"D. Bj\u00f8rner","year":"2004","unstructured":"Bj\u00f8rner, D.: Domain engineering: a \u201cRadical innovation\u201d for software and systems engineering? A biased account. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 100\u2013144. Springer, Heidelberg (2004)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: A declarative language for programming synchronous systems. In: POPL, pp. 178\u2013188 (1987)","DOI":"10.1145\/41625.41641"},{"key":"5_CR6","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.A., 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.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Raymond, P., Ratel, C.: Generating Efficient Code From Data-Flow Programs. In: PLILP, vol.\u00a022, pp. 207\u2013218 (1991); special Issue on WOFACS 1998","DOI":"10.1007\/3-540-54444-5_100"},{"issue":"5","key":"5_CR8","first-page":"669","volume":"13","author":"A. Hall","year":"2007","unstructured":"Hall, A.: Realising the benefits of formal methods. J. UCS\u00a013(5), 669\u2013678 (2007)","journal-title":"J. UCS"},{"key":"5_CR9","unstructured":"IEC 61131 Programmable controllers, www.iec.ch"},{"issue":"4","key":"5_CR10","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1145\/1498765.1498787","volume":"52","author":"D. Jackson","year":"2009","unstructured":"Jackson, D.: A Direct Path to Dependable Software. Commun. ACM\u00a052(4), 78\u201388 (2009)","journal-title":"Commun. ACM"},{"key":"5_CR11","volume-title":"Software Requirements & Specifications: A Lexicon of Practice, Principles and Prejudices","author":"M. Jackson","year":"1995","unstructured":"Jackson, M.: Software Requirements & Specifications: A Lexicon of Practice, Principles and Prejudices. ACM Press\/Addison-Wesley Publishing Co., New York, NY, USA (1995)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Jackson, M., Zave, P.: Deriving specifications from requirements: An example. In: ICSE, pp. 15\u201324 (1995)","DOI":"10.1145\/225014.225016"},{"key":"5_CR13","volume-title":"Systematic software development using VDM","author":"C.B. Jones","year":"1986","unstructured":"Jones, C.B.: Systematic software development using VDM. Prentice Hall International (UK) Ltd., Hertfordshire (1986)"},{"issue":"5","key":"5_CR14","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1109\/TSE.1981.230854","volume":"7","author":"E. Kant","year":"1981","unstructured":"Kant, E., Barstow, D.R.: The refinement paradigm: The interaction of coding and efficiency knowledge in program synthesis. IEEE Trans. Software Eng.\u00a07(5), 458\u2013471 (1981)","journal-title":"IEEE Trans. Software Eng."},{"key":"5_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1494-9","volume-title":"The B Language and Method: A Guide to Practical Formal Development","author":"K. Lano","year":"1996","unstructured":"Lano, K.: The B Language and Method: A Guide to Practical Formal Development. Springer, New York (1996)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1007\/978-3-642-05089-3_51","volume-title":"FM 2009: Formal Methods","author":"D. Leinenbach","year":"2009","unstructured":"Leinenbach, D., Santen, T.: Verifying the microsoft hyper-V hypervisor with VCC. In: Cavalcanti, A., Dams, D. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 806\u2013809. Springer, Heidelberg (2009)"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1234741.1234762","volume":"32","author":"M.R. Nami","year":"2007","unstructured":"Nami, M.R., Tehrani, M.S., Sharifi, M.: Applying domain engineering using raise into a particular banking domain. SIGSOFT Softw. Eng. Notes\u00a032(2), 1\u20136 (2007)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"2","key":"5_CR18","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s00766-007-0048-y","volume":"12","author":"R. Seater","year":"2007","unstructured":"Seater, R., Jackson, D., Gheyi, R.: Requirement Progression in Problem Frames: Deriving Specifications from Requirements. Requir. Eng.\u00a012(2), 77\u2013102 (2007)","journal-title":"Requir. Eng."},{"issue":"4","key":"5_CR19","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/S0950-5849(00)00166-X","volume":"43","author":"C.F. Snook","year":"2001","unstructured":"Snook, C.F., Harrison, R.: Practitioners\u2019 views on the use of formal methods: an industrial survey by structured interview. Information & Software Technology\u00a043(4), 275\u2013283 (2001)","journal-title":"Information & Software Technology"},{"key":"5_CR20","unstructured":"The RAISE Method Group: The RAISE Development Method. The BCS Practitioners Series, Prentice-Hall International, Englewood Cliffs (1995)"},{"key":"5_CR21","unstructured":"The Verifying C Compiler at Codeplex, http:\/\/vcc.codeplex.com\/"},{"key":"5_CR22","unstructured":"Microsoft Visual Studio at MSDN, http:\/\/msdn.microsoft.com\/en-us\/vstudio\/default.aspx"},{"key":"5_CR23","unstructured":"Westphal, B., Dietsch, D., Podelski, A., Pahlow, L.: Successful software subcontracting by system verification (submitted)"},{"issue":"4","key":"5_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J. Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv.\u00a041(4), 1\u201336 (2009)","journal-title":"ACM Comput. Surv."}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T00:07:14Z","timestamp":1560298034000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}