{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:29:27Z","timestamp":1743103767545,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319079943"},{"type":"electronic","value":"9783319079950"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-07995-0_44","type":"book-chapter","created":{"date-parts":[[2014,6,10]],"date-time":"2014-06-10T23:24:31Z","timestamp":1402442671000},"page":"443-452","source":"Crossref","is-referenced-by-count":4,"title":["A Survey on Static Analysis and Model Checking"],"prefix":"10.1007","author":[{"given":"Iv\u00e1n","family":"Garc\u00eda-Ferreira","sequence":"first","affiliation":[]},{"given":"Carlos","family":"Laorden","sequence":"additional","affiliation":[]},{"given":"Igor","family":"Santos","sequence":"additional","affiliation":[]},{"given":"Pablo Garc\u00eda","family":"Bringas","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"44_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-48320-9_8","volume-title":"CONCUR\u201999. Concurrency Theory","author":"R. Alur","year":"1999","unstructured":"Alur, R., de Alfaro, L., Henzinger, T.A., Mang, F.Y.C.: Automating Modular Verification. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, p. 82. Springer, Heidelberg (1999)"},{"key":"44_CR2","unstructured":"ARC, \n                    http:\/\/altarica.labri.fr\/wp\/?page_id=32\n                   (last accessed February 20, 2014)"},{"key":"44_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-24723-4_2","volume-title":"Compiler Construction","author":"G. Balakrishnan","year":"2004","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol.\u00a02985, pp. 5\u201323. Springer, Heidelberg (2004)"},{"key":"44_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-69149-5_22","volume-title":"Verified Software: Theories, Tools, Experiments","author":"G. Balakrishnan","year":"2008","unstructured":"Balakrishnan, G., Reps, T., Melski, D., Teitelbaum, T.: WYSINWYX: What You See Is Not What You eXecute. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 202\u2013213. Springer, Heidelberg (2008)"},{"issue":"3","key":"44_CR5","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica\u00a020(3), 207\u2013226 (1983)","journal-title":"Acta Informatica"},{"key":"44_CR6","doi-asserted-by":"crossref","unstructured":"Christodorescu, M., Jha, S., Seshia, S.A., Song, D., Bryant, R.E.: Semantics-aware malware detection. In: Proc. IEEE Symposium on Security and Privacy, pp. 32\u201346 (2005)","DOI":"10.1109\/SP.2005.20"},{"key":"44_CR7","doi-asserted-by":"crossref","unstructured":"Christodorescu, M., Jha, S.: Static analysis of executables to detect malicious patterns. Wisconsin Univ-Madison dept of Computer Sciences (2006)","DOI":"10.21236\/ADA449067"},{"key":"44_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"issue":"2","key":"44_CR9","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"44_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pp. 294\u2013303. ACM (December 1987)","DOI":"10.1145\/41840.41865"},{"key":"44_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-44577-3_12","volume-title":"Informatics","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol.\u00a02000, pp. 176\u2013194. Springer, Heidelberg (2001)"},{"key":"44_CR12","unstructured":"CodeSurfer, \n                    http:\/\/www.grammatech.com\/research\/technologies\/codesurfer\n                   (last accessed February 20, 2014)"},{"key":"44_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"1","key":"44_CR14","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P. Cousot","year":"1999","unstructured":"Cousot, P., Cousot, R.: Refining Model Checking by Abstract Interpretation. Automated Software Engineering Journal\u00a06(1), 69\u201395 (1999)","journal-title":"Automated Software Engineering Journal"},{"key":"44_CR15","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of program. Communications of the ACM, 453\u2013457 (1975)","DOI":"10.1145\/360933.360975"},{"issue":"7","key":"44_CR16","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V. D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a027(7), 1165\u20131178 (2008)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"44_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E.A. Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol.\u00a085, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"key":"44_CR18","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Halpern, J.Y.: Decisions procedures and expressiveness in the temporal logic of branching time. In: Handbook of Theorical Computer Science, vol.\u00a0B: Formal models and Semantics. Elsevier (1985)","DOI":"10.1016\/0022-0000(85)90001-7"},{"issue":"1","key":"44_CR19","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: Sometimes and not never revisited: on branching versus linear time temporal logic. Journal of the ACM (JACM)\u00a033(1), 151\u2013178 (1986)","journal-title":"Journal of the ACM (JACM)"},{"key":"44_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-540-24622-0_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Engler","year":"2004","unstructured":"Engler, D., Musuvathi, M.: Static analysis versus software model checking for bug finding. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 191\u2013210. Springer, Heidelberg (2004)"},{"key":"44_CR21","unstructured":"F.L.I.R.T., \n                    https:\/\/www.hex-rays.com\/products\/ida\/tech\/flirt\/index.shtml\n                   (last accessed February 20, 2014)"},{"key":"44_CR22","unstructured":"Frama-C, \n                    http:\/\/frama-c.com\/\n                   (last accessed February 20, 2014)"},{"key":"44_CR23","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Commun. ACM\u00a012 (1969)","DOI":"10.1145\/363235.363259"},{"key":"44_CR24","unstructured":"Holzman, G.J.: Design and validation of computer protocols. Prentice-Hall (1990)"},{"key":"44_CR25","unstructured":"IDA Pro, \n                    https:\/\/www.hex-rays.com\/products\/ida\/\n                   (last accessed February 20, 2014)"},{"key":"44_CR26","unstructured":"Java+ITP, \n                    http:\/\/maude.cs.uiuc.edu\/tools\/javaitp\/\n                   (last accessed February 20, 2014)"},{"key":"44_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/11506881_11","volume-title":"Intrusion and Malware Detection and Vulnerability Assessment","author":"J. Kinder","year":"2005","unstructured":"Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Detecting malicious code by model checking. In: Julisch, K., Kruegel, C. (eds.) DIMVA 2005. LNCS, vol.\u00a03548, pp. 174\u2013187. Springer, Heidelberg (2005)"},{"key":"44_CR28","unstructured":"Konur, S.: A survey on temporal logics. arXiv preprint (2010)"},{"key":"44_CR29","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Result on the Propositional \u03bc-calculus. Journal of Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Journal of Theoretical Computer Science"},{"key":"44_CR30","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"N.. Leveson","year":"1993","unstructured":"Leveson, N.: An Investigation of the Therac-25 Accidents. IEEE Computer\u00a026, 18\u201341 (1993)","journal-title":"IEEE Computer"},{"key":"44_CR31","unstructured":"Lions, J.L.: ARIANE 5, Flight 501 Failure (1993), \n                    http:\/\/www.di.unito.it\/~damiani\/ariane5rep.html\n                   (last accessed February 20, 2014)"},{"key":"44_CR32","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer (1991)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"44_CR33","unstructured":"mCRL2, \n                    http:\/\/www.mcrl2.org\/\n                   (last accessed February 20, 2014)"},{"key":"44_CR34","unstructured":"NuSMV, \n                    http:\/\/nusmv.fbk.eu\/\n                   (last accessed February 20, 2014)"},{"key":"44_CR35","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science 18th (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"44_CR36","unstructured":"Predator, \n                    http:\/\/www.fit.vutbr.cz\/research\/groups\/verifit\/tools\/predator\/\n                   (last accessed February 20, 2014)"},{"key":"44_CR37","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"44_CR38","unstructured":"Reynolds, J.: Automatic computation of data set definitions. Science (1967)"},{"key":"44_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-642-32759-9_34","volume-title":"FM 2012: Formal Methods","author":"F. Song","year":"2012","unstructured":"Song, F., Touili, T.: Efficient malware detection using model-checking. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 418\u2013433. Springer, Heidelberg (2012)"},{"key":"44_CR40","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: PoMMaDe: pushdown model-checking for malware detection. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, pp. 607\u2013610. ACM (August 2013)","DOI":"10.1145\/2491411.2494599"},{"key":"44_CR41","unstructured":"SPIN, \n                    http:\/\/spinroot.com\/spin\/whatispin.html\n                   (last accessed February 20, 2014)"},{"key":"44_CR42","unstructured":"The First Computer Bug, \n                    http:\/\/www.history.navy.mil\/photos\/images\/h96000\/h96566kc.htm\n                   (last accessed February 20, 2014)"}],"container-title":["Advances in Intelligent Systems and Computing","International Joint Conference SOCO\u201914-CISIS\u201914-ICEUTE\u201914"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07995-0_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,19]],"date-time":"2023-01-19T21:15:54Z","timestamp":1674162954000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-07995-0_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319079943","9783319079950"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07995-0_44","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2014]]}}}