{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:46:26Z","timestamp":1725561986127},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212997"},{"type":"electronic","value":"9783540247302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24730-2_7","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T11:00:15Z","timestamp":1280746815000},"page":"93-107","source":"Crossref","is-referenced-by-count":11,"title":["Automatic Creation of Environment Models via Training"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladimir","family":"Levin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fei","family":"Xie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"7_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. TOPLAS: Transactions on Programming Languages and Systems\u00a017(3), 507\u2013535 (1995)","journal-title":"TOPLAS: Transactions on Programming Languages and Systems"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. Formal Methods in System Design\u00a015, 7\u201348 (1999)","journal-title":"Formal Methods in System Design"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/378795.378846","volume-title":"PLDI 2001: Programming Language Design and Implementation","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI 2001: Programming Language Design and Implementation, pp. 203\u2013213. ACM, New York (2001)"},{"key":"7_CR4","unstructured":"Ball, T., Millstein, T., Rajamani, S.K.: Polymorphic predicate abstraction. Technical Report MSR-TR-2001-10, Microsoft Research (2001)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"7_CR6","unstructured":"Ball, T., Rajamani, S.K.: Generating abstract explanations of spurious counterexamples in C programs. Technical Report MSR-TR-2002-09, Microsoft Research (January 2002)"},{"key":"7_CR7","first-page":"1","volume-title":"POPL 2002: Principles of Programming Languages","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: POPL 2002: Principles of Programming Languages, January 2002, pp. 1\u20133. ACM, New York (2002)"},{"key":"7_CR8","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder - a second generation of a Java model checker. In: Workshop on Advances in Verification (2000)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Workshop on Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logic of Programs. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"7_CR10","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"issue":"2","key":"7_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/32.908957","volume":"27","author":"M.D. Ernst","year":"2001","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions in Software Engineering\u00a027(2), 1\u201325 (2001)","journal-title":"IEEE Transactions in Software Engineering"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","first-page":"421","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Harel, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 421\u2013427. Springer, Heidelberg (1996)"},{"issue":"5","key":"7_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The Spin model checker. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"7_CR15","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1109\/TSE.2002.995426","volume":"28","author":"G.J. Holzmann","year":"2002","unstructured":"Holzmann, G.J., Smith, M.H.: An automated verification method for distributed systems software based on model extraction. IEEE Transactions on Software Engineering\u00a028(4), 364\u2013377 (2002)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"7_CR17","unstructured":"McMillan, K.L.: A methodology for hardware verification using compositional model checking. Cadence TR (1999)"},{"key":"7_CR18","volume-title":"Executable UML: A Foundation for Model Driven Architecture","author":"S.J. Mellor","year":"2002","unstructured":"Mellor, S.J., Balcer, M.J.: Executable UML: A Foundation for Model Driven Architecture. Addison-Wesley, Reading (2002)"},{"key":"7_CR19","volume-title":"Programming the Microsoft Windows Driver Model","author":"W. Oney","year":"2003","unstructured":"Oney, W.: Programming the Microsoft Windows Driver Model. Microsoft Press, Redmond (2003)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular reasoning about programs. In: Logics and Models of Concurrent Systems. NATO ASI Series (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Quielle","year":"1982","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"7_CR22","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/ASE.2000.873645","volume-title":"ASE 2000: Automated Software Engineering","author":"W. Visser","year":"2000","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.J.: Model checking programs. In: ASE 2000: Automated Software Engineering, pp. 3\u201312. IEEE, Los Alamitos (2000)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24730-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,17]],"date-time":"2019-03-17T15:00:06Z","timestamp":1552834806000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24730-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212997","9783540247302"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24730-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}