{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:07:32Z","timestamp":1725487652003},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540695066"},{"type":"electronic","value":"9783540695073"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-69507-3_78","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T13:35:58Z","timestamp":1184592958000},"page":"900-910","source":"Crossref","is-referenced-by-count":1,"title":["Extracting Zing Models from C Source Code"],"prefix":"10.1007","author":[{"given":"Tomas","family":"Matousek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Filip","family":"Zavoral","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"78_CR1","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/978-3-540-27813-9_42","volume-title":"Computer Aided Verification","author":"Tony Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A Model Checker for Concurrent Software. Technical Report, Microsoft Research (2004)"},{"key":"78_CR2","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"78_CR3","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Z.H.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proceedings of the International Conference on Software Engineering, ICSE (2000)","DOI":"10.1145\/337180.337234"},{"key":"78_CR4","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of the 21st\u00a0International Conference on Software Engineering, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"78_CR5","unstructured":"Dwyer, M.B., Hatcliff, J.: Slicing Software for Model Construction. Journal of High-Order and Symbolic Computation (2000)"},{"key":"78_CR6","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer Analysis: Haven\u2019t We Solved this Problem Yet? In: 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE\u201901 (2001)","DOI":"10.1145\/379605.379665"},{"key":"78_CR7","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)"},{"key":"78_CR8","unstructured":"ISO: C99 \u2013 The C Programming Language Standard (ISO\/IEC 9899:1999)"},{"key":"78_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-Prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"78_CR10","unstructured":"Krinke, J.: Advanced Slicing of Sequential and Concurrent Programs. PhD Thesis, Fakult\u00e4t F\u00fcr Mathematik und Informatik, Universit\u00e4t Passau (2003)"},{"key":"78_CR11","unstructured":"Matousek, T.: Model of the Windows Driver Environment. Master Thesis at Department of Software Engineering, Charles University in Prague (2005), http:\/\/nenya.ms.mff.cuni.cz\/publications\/Matousek-thesis.pdf"},{"key":"78_CR12","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking \u2013 an Approach to the State Explosion Problem. PhD Thesis, SCS, Carnegie Mellon University (1992)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"78_CR13","unstructured":"Microsoft: NET Framework, MSDN, http:\/\/msdn.microsoft.com\/netframework"},{"key":"78_CR14","unstructured":"Microsoft: PREfast, http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/PREfast.mspx"},{"key":"78_CR15","unstructured":"Microsoft: Static Driver Verifier \u2013 Finding Driver Bugs at Compile-Time, WHDC, http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/sdv.mspx"},{"key":"78_CR16","unstructured":"Microsoft: Windows Driver Foundation, WHDC, http:\/\/www.microsoft.com\/whdc\/driver\/wdf\/default.mspx"},{"key":"78_CR17","unstructured":"Microsoft Research: SLAM Project, http:\/\/research.microsoft.com\/slam"},{"key":"78_CR18","unstructured":"Microsoft Research: Zing Model Checker, http:\/\/research.microsoft.com\/zing"},{"key":"78_CR19","unstructured":"NASA Intelligent Systems Division: Java Path Finder, http:\/\/ase.arc.nasa.gov\/havelund\/jpf.html"},{"key":"78_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate Language and tools for Analysis and Transformation of C Programs. In: Horspool, R.N. (ed.) CC 2002 and ETAPS 2002. LNCS, vol.\u00a02304, pp. 209\u2013265. Springer, Heidelberg (2002)"},{"key":"78_CR21","unstructured":"Necula, G.C., McPeak, S., Weimer, W., Harren, M., Condit, J.: CCured, http:\/\/manju.cs.berkeley.edu\/ccured"},{"key":"78_CR22","unstructured":"Perens, B.: ElecticFence, http:\/\/perens.com\/FreeSoftware\/ElectricFence"},{"issue":"5","key":"78_CR23","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1145\/949952.940107","volume":"28","author":"Robby","year":"2003","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An Extensible and Highly Modular Software Model Checking Framework. SIGSOFT Softw. Eng. Notes\u00a028(5), 267\u2013276 (2003)","journal-title":"SIGSOFT Softw. Eng. Notes"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2007: Theory and Practice of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69507-3_78","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T00:01:33Z","timestamp":1556668893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69507-3_78"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540695066","9783540695073"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69507-3_78","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}