{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:13:11Z","timestamp":1768000391245,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642407864","type":"print"},{"value":"9783642407871","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40787-1_15","type":"book-chapter","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T23:18:35Z","timestamp":1379546315000},"page":"251-268","source":"Crossref","is-referenced-by-count":13,"title":["To Run What No One Has Run Before: Executing an Intermediate Verification Language"],"prefix":"10.1007","author":[{"given":"Nadia","family":"Polikarpova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott","family":"West","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"15_CR1","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1721654.1721675","volume":"53","author":"S. Antoy","year":"2010","unstructured":"Antoy, S., Hanus, M.: Functional logic programming. Commun. ACM\u00a053(4), 74\u201385 (2010)","journal-title":"Commun. ACM"},{"issue":"2","key":"15_CR2","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C. Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM\u00a056(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"15_CR6","unstructured":"Furia, C.A., Meyer, B., Velder, S.: Loop invariants: Analysis, classification, and examples (2012), \n                    \n                      http:\/\/arxiv.org\/abs\/1211.4470"},{"key":"15_CR7","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2006)"},{"key":"15_CR8","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (August 2008)"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Kiselyov, O., Shan, C.-C., Friedman, D.P., Sabry, A.: Backtracking, interleaving, and terminating monad transformers (functional pearl). In: ICFP, pp. 192\u2013203. ACM (2005)","DOI":"10.1145\/1090189.1086390"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V. Klebanov","year":"2011","unstructured":"Klebanov, V., et al.: The 1st verified software competition: Experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 154\u2013168. Springer, Heidelberg (2011)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: SOSP, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"K\u00f6ksal, A., Kuncak, V., Suter, P.: Constraints as control. In: POPL, pp. 151\u2013164 (2012)","DOI":"10.1145\/2103621.2103675"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI, pp. 316\u2013329. ACM (2010)","DOI":"10.1145\/1809028.1806632"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-24690-6_28","volume-title":"Software Engineering and Formal Methods","author":"C. Goues Le","year":"2011","unstructured":"Le Goues, C., Leino, K.R.M., Moskal, M.: The boogie verification debugger (Tool paper). In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol.\u00a07041, pp. 407\u2013414. Springer, Heidelberg (2011)"},{"issue":"1-3","key":"15_CR15","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"G.T. Leavens","year":"2005","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program.\u00a055(1-3), 185\u2013208 (2005)","journal-title":"Sci. Comput. Program."},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1007\/978-3-642-05089-3_51","volume-title":"FM 2009: Formal Methods","author":"D. Leinenbach","year":"2009","unstructured":"Leinenbach, D., Santen, T.: Verifying the microsoft hyper-V hypervisor with VCC. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 806\u2013809. Springer, Heidelberg (2009)"},{"key":"15_CR17","unstructured":"Leino, K.R.M.: This is Boogie 2 (2008), \n                    \n                      http:\/\/goo.gl\/QsH6g"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"15_CR19","unstructured":"Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Workshop (2010), \n                    \n                      http:\/\/fm.csl.sri.com\/UV10\/"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Rayside, D., Yessenov, K., Jackson, D.: Unifying execution of imperative and declarative code. In: ICSE, pp. 511\u2013520. ACM (2011)","DOI":"10.1145\/1985793.1985863"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-21437-0_8","volume-title":"FM 2011: Formal Methods","author":"P. M\u00fcller","year":"2011","unstructured":"M\u00fcller, P., Ruskiewicz, J.N.: Using debuggers to understand failed verification attempts. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 73\u201387. Springer, Heidelberg (2011)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Pattis, R.E.: Textbook errors in binary searching. In: SIGCSE, pp. 190\u2013194. ACM (1988)","DOI":"10.1145\/52965.53012"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Furia, C.A., Pei, Y., Wei, Y., Meyer, B.: What good are strong specifications? In: ICSE, pp. 257\u2013266. ACM (2013)","DOI":"10.1109\/ICSE.2013.6606572"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-23702-7_23","volume-title":"Static Analysis","author":"P. Suter","year":"2011","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 298\u2013315. Springer, Heidelberg (2011)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-642-24690-6_26","volume-title":"Software Engineering and Formal Methods","author":"J. Tschannen","year":"2011","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable verification of object-oriented programs by combining static and dynamic techniques. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol.\u00a07041, pp. 382\u2013398. Springer, Heidelberg (2011)"},{"key":"15_CR26","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Verifying Eiffel programs with Boogie. In: BOOGIE Workshop (2011), \n                    \n                      http:\/\/arxiv.org\/abs\/1106.4700"},{"key":"15_CR27","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Program checking with less hassle. In: VSTTE (to appear, 2013)"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-77395-5_17","volume-title":"Runtime Verification","author":"K. Zee","year":"2007","unstructured":"Zee, K., Kuncak, V., Taylor, M., Rinard, M.C.: Runtime checking for program verification. In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol.\u00a04839, pp. 202\u2013213. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40787-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T11:24:08Z","timestamp":1558092248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40787-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642407864","9783642407871"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40787-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}