{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:43:33Z","timestamp":1773654213823,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540781622","type":"print"},{"value":"9783540781639","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78163-9_15","type":"book-chapter","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T05:30:06Z","timestamp":1204263006000},"page":"142-156","source":"Crossref","is-referenced-by-count":13,"title":["Extending Model Checking with Dynamic Analysis"],"prefix":"10.1007","author":[{"given":"Alex","family":"Groce","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Joshi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T.: The concept of dynamic analysis. In: European Software Engineering Conference\/Foundations of Software Engineering, pp. 216\u2013234 (1999)","DOI":"10.1007\/3-540-48166-4_14"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Nethercote, N., Seward, J.: Valgrind: A framework for heavyweight dynamic binary instrumentation. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2007)","DOI":"10.1145\/1250734.1250746"},{"key":"15_CR3","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Kroening, D., Clarke, E.M., Lerda, F.: A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 168\u2013176 (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: SPIN Workshop on Model Checking of Software, pp. 103\u2013122 (2001)","DOI":"10.1007\/3-540-45139-0_7"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., et al.: CMC: A pragmatic approach to model checking real code. In: Symposium on Operating System Design and Implementation (2002)","DOI":"10.1145\/1060289.1060297"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven software verification. In: SPIN Workshop on Model Checking of Software, pp. 76\u201391 (2004)","DOI":"10.1007\/978-3-540-24732-6_6"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Groce, A., Holzmann, G., Joshi, R.: Randomized differential testing as a prelude to formal verification. In: International Conference on Software Engineering (2007)","DOI":"10.1109\/ICSE.2007.68"},{"key":"15_CR9","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, Reading (2003)"},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G.J. Holzmann","year":"2007","unstructured":"Holzmann, G.J., Bosnacki, D.: The design of a multi-core extension of the Spin model checker. IEEE Transactions on Software Engineering\u00a033, 659\u2013674 (2007)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR11","unstructured":"Leino, K.R.M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology (1995)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Necula, G., et al.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: International Conference on Compiler Construction, pp. 213\u2013228 (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Flanagan, C., et al.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"15_CR14","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer\u00a07, 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"15_CR15","unstructured":"Wing, J.M.: A two-tiered approach to specifying programs (1983)"},{"key":"15_CR16","unstructured":"Various: A collection of NAND Flash application notes, whitepapers and articles, http:\/\/www.data-io.com\/NAND\/NANDApplicationNotes.asp"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Person, S., Elbaum, S.G.: Controlling factors in evaluating path-sensitive error detection techniques. In: Foundations of Software Engineering, pp. 92\u2013104 (2006)","DOI":"10.21236\/ADA459081"},{"key":"15_CR18","unstructured":"IBM\u00a0Rational\u00a0Software: Purify: Advanced runtime error checking for C\/C++ developers, http:\/\/www-306.ibm.com\/software\/awdtools\/purify\/"},{"key":"15_CR19","unstructured":"Cowan, C., et al.: StackGuard: Automatic adaptive detection and prevention of buffer-overflow attacks. In: Proc. 7th USENIX Security Conference, pp. 63\u201378 (1998)"},{"key":"15_CR20","unstructured":"Musuvathi, M.: Email communications (2007)"},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., et al.: Model checking programs. Automated Software Engineering\u00a010(2), 203\u2013232 (2003)","journal-title":"Automated Software Engineering"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Ernst, M., et al.: Dynamically discovering likely program invariants to support program evolution. In: International Conference on Software Engineering, pp. 213\u2013224 (1999)","DOI":"10.1145\/302405.302467"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: SPIN Workshop on Model Checking of Software, pp. 121\u2013135 (2003)","DOI":"10.1007\/3-540-44829-2_8"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Verisoft: A tool for the automatic analysis of concurrent software. In: Computer-Aided Verification, pp. 172\u2013186 (1997)","DOI":"10.1007\/3-540-63166-6_52"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Kroening, D., Groce, A., Clarke, E.M.: Counterexample guided abstraction refinement via program execution. In: International Conference on Formal Engineering Methods, pp. 224\u2013238 (2004)","DOI":"10.1007\/978-3-540-30482-1_23"},{"key":"15_CR26","unstructured":"Havelund, K., Goldberg, A.: Verify your runs. In: Verified Software: Theories, Tools, Experiments (2005)"},{"key":"15_CR27","unstructured":"Havelund, K.: RMOR Version 2.0 user manual. Kestrel Technology, California, USA (2006)"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Yang, J., et al.: Perracotta: Mining temporal API rules from imperfect traces. In: International Conference on Software Engineering, pp. 282\u2013291 (2006)","DOI":"10.1145\/1134285.1134325"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Yang, J., Evans, D.: Dynamically inferring temporal properties. In: Workshop on Program Analysis For Software Tools and Engineering, pp. 23\u201328 (2004)","DOI":"10.1145\/996821.996832"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78163-9_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:00:33Z","timestamp":1619506833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78163-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781622","9783540781639"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78163-9_15","relation":{},"subject":[]}}