{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214179},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_26","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"379-384","source":"Crossref","is-referenced-by-count":7,"title":["The KeY system 1.0 (Deduction Component)"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[]},{"given":"Martin","family":"Giese","sequence":"additional","affiliation":[]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[]},{"given":"Vladimir","family":"Klebanov","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]},{"given":"Steffen","family":"Schlager","sequence":"additional","affiliation":[]},{"given":"Peter H.","family":"Schmitt","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings, Testing and Proofs, Z\u00fcrich, Switzerland","author":"B. Beckert","year":"2007","unstructured":"Beckert, B., Gladisch, C.: White-box testing by combining deduction-based specification extraction and black-box testing. In: Gurevich, Y. (ed.) Proceedings, Testing and Proofs, Z\u00fcrich, Switzerland. LNCS, Springer, Heidelberg (2007)"},{"key":"26_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/978-3-540-32004-3_20","volume-title":"Security in Pervasive Computing","author":"\u00c1. Darvas","year":"2005","unstructured":"Darvas, \u00c1., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol.\u00a03450, pp. 193\u2013209. Springer, Heidelberg (2005)"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-75209-7","volume-title":"Proceedings, Testing and Proofs","author":"C. Engel","year":"2007","unstructured":"Engel, C., H\u00e4hnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y. (ed.) Proceedings, Testing and Proofs, Z\u00fcrich, Switzerland. LNCS, Springer, Heidelberg (2007)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11557432_23","volume-title":"Model Driven Engineering Languages and Systems","author":"M. Giese","year":"2005","unstructured":"Giese, M., Larsson, D.: Simplifying transformations of OCL constraints. In: Briand, L.C., Williams, C. (eds.) MoDELS 2005. LNCS, vol.\u00a03713, Springer, Heidelberg (2005)"},{"key":"26_CR6","volume-title":"Proc. of the 4th Workshop on Java Technologies for Real-time and Embedded Systems (JTRES)","author":"J.J. Hunt","year":"2006","unstructured":"Hunt, J.J., Jenn, E., Leriche, S., Schmitt, P., Tonin, I., Wonnemann, C.: A case study of specification and verification using JML in an avionics application. In: Rochard-Foy, M., Wellings, A. (eds.) Proc. of the 4th Workshop on Java Technologies for Real-time and Embedded Systems (JTRES), ACM Press, New York (2006)"},{"key":"26_CR7","unstructured":"Nanchen, S., Schmid, H., Schmitt, P., St\u00e4rk, R.F.: The ASMKeY prover. Technical Report 436, Department of Computer Science, ETH Z\u00fcrich (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:06Z","timestamp":1619517186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}