{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:27:10Z","timestamp":1754486830353},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540666240"},{"type":"electronic","value":"9783540480921"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48092-7_14","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T13:01:46Z","timestamp":1186750906000},"page":"319-319","source":"Crossref","is-referenced-by-count":11,"title":["Verification of Automotive Control Units"],"prefix":"10.1007","author":[{"given":"Tom","family":"Bienm\u00fcllor","sequence":"first","affiliation":[]},{"given":"J\u00fcrgon","family":"Bohn","sequence":"additional","affiliation":[]},{"given":"Henning","family":"Brinkmann","sequence":"additional","affiliation":[]},{"given":"Udo","family":"Brockmeyer","sequence":"additional","affiliation":[]},{"given":"Werner","family":"Damm","sequence":"additional","affiliation":[]},{"given":"Hardi","family":"Hungar","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Jansen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,3,24]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Torn Bienm\u00fcller, Udo Brockmeyer, Werner Damm, Gert D\u00f6hmen, Claus E\u03b2mann, Hans-J\u00fcrgen Holberg, Hardi Hungar, Bernhard Josko, Rainer Schl\u00f6r, Gunnar Wittich, Hartmut Wittke, Geoffrey Clements, John Rowlands, and Eric Sefton. Formal Verification of au Avionics Application using Abstraction and Symbolic Model Checking. In Felix Redmill and Tom Anderson, editors, Towards System Safety Proccedings of the Seventh SafetY-Proceedings of the Seventh Safety-Critical Systems Symposium. Huntingdon. UK, pages 150\u2013173. Safety-Critical Systems Club, Springer Verlag, 1999.","DOI":"10.1007\/978-1-4471-0823-8_10"},{"key":"14_CR2","series-title":"Lect Notes Comput Sci","first-page":"260","volume-title":"Property preserving simulations","author":"S. Bensalem","year":"1992","unstructured":"S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property preserving simulations. In G.v. Bachmann and D.K. Probst, editors, 4th Int. Workshop on Computer Aided Verification, LNCS 663, pages 260\u2013273. Springer, 1992."},{"key":"14_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/978-3-540-49382-2_27","volume-title":"FSTTCS 98","author":"J. Bohn","year":"1998","unstructured":"J. Bohn, W. Damm, O. Grumberg, H. Hungar, and K. Laster. First-order CTL model checking. In V. Arvind and R. Ramanujam, editors, FSTTCS 98, LNCS 1530, pages 283\u2013294, 1998."},{"key":"14_CR4","unstructured":"Henning Brinkmann. Verifikation eines hybriden Steuersystems mit Hilfe erweiterter Abstraktiosmethoen. Master's thesis, Carl von Ossietzky Universitat Oldenburg, February 1999."},{"key":"14_CR5","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. B. Bryant","year":"1992","unstructured":"Randal B. Bryant. Symbolic boolean Manipulation with ordered Binary-Decision Diagrams. ACM Comp. Surveys. 24:293\u2013318, 1992.","journal-title":"ACM Comp. Surveys"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke, B.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In Proccedings of the 10th ACM Symposium on Principles of Programming Languages, pages 117\u2013126, 1983.","DOI":"10.1145\/567067.567080"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"1G","author":"E. M. Clarke","year":"1994","unstructured":"Edmund M. Clarke, Oma Grumberg, and David B. Long. Model checking and abstraction. In ACM Transactions on Programming Languages and Systems, volume 1G, pages 1512\u20131542, September 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/3-540-49213-5_8","volume-title":"Proceedings. International Symposium on Compositionality The Significant Difference","author":"W. Damm","year":"1998","unstructured":"Werner Damm, Bernhard Jeske, Hardi Hungar, and Amir Pnueli. A compositional real-time semantics of STATEMATE designs. In W.-P. de Roever, editor, Proceedings. International Symposium on Compositionality The Significant Difference, LNCS 153G, pages 186\u2013238. Springer-Verlag, 1998."},{"key":"14_CR9","unstructured":"W. Damm, B. Jeske, and R. Sch\u00f6ldr. Specification and verification of VHDL-based system-level hardware designs. In E. B\u00f6rger, editor, SpeCification and Validition Methods, pages 331\u2013410. Oxford Univ. Press, 1995."},{"key":"14_CR10","series-title":"Lect Notes Comput Sci","first-page":"120","volume-title":"CHARME 95","author":"H. Hungar","year":"1995","unstructured":"H. Hungar, O. Grumberg, and W. Damm. what if model checking must be truly symbolic. In P. Camurati and H. Eveking, editors, CHARME 95, LNCS 987, pages 120. Springer Verlag, 1995."},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"T.A. Henzinger, P.-H. He, and H. Wong-Toi. HyTech: A model checker for hybrid systems. SoftwaTe Tools fOT Technology Transfer, 1:110\u2013122, 1997.","journal-title":"SoftwaTe Tools fOT Technology Transfer"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576\u2013583, 1969.","journal-title":"Communications of the ACM"},{"key":"14_CR13","unstructured":"Bernhard Josk0. Modular Specification and Verification of Reactive terms. Carl von Ossietzky Universitat Oldenburg, 1993. Habiltaticnsschrift."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Formal verification in a commercial setting. In Proc. 84th Design Automation Conference, pages 258\u2013262, 1997.","DOI":"10.1109\/DAC.1997.597154"},{"key":"14_CR15","unstructured":"Kenneth L. Mckdillan. Symbohc Model Checking. Kluwer Academic Publishers, 1993."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic. In Procecdinqs of the 18th Annual ACAf Symposium in Principles of Programmking Languages, pages 184\u2013193, 1986.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Correct System Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48092-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:23:28Z","timestamp":1556735008000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48092-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540666240","9783540480921"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48092-7_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}