{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:40:02Z","timestamp":1744206002467,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642340253"},{"type":"electronic","value":"9783642340260"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-34026-0_24","type":"book-chapter","created":{"date-parts":[[2012,9,26]],"date-time":"2012-09-26T01:07:20Z","timestamp":1348621640000},"page":"312-326","source":"Crossref","is-referenced-by-count":17,"title":["A Unified Approach for Static and Runtime Verification: Framework and Applications"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Ahrendt","sequence":"first","affiliation":[]},{"given":"Gordon J.","family":"Pace","sequence":"additional","affiliation":[]},{"given":"Gerardo","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Ahrendt, W.: Using KeY. In: Beckert et al. [11], pp. 409\u2013451","DOI":"10.1007\/978-3-540-69061-0_10"},{"key":"24_CR2","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W. Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling\u00a04, 32\u201354 (2005)","journal-title":"Software and System Modeling"},{"key":"24_CR3","unstructured":"Aktug, I., Naliuka, K.: Conspec: A formal language for policy specification. In: FLACOS 2007, Oslo, Norway, pp. 107\u2013109 (October 2007)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-92188-2_5","volume-title":"Formal Methods for Components and Objects","author":"E. Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 113\u2013132. Springer, Heidelberg (2008)"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/1103845.1094839","volume":"40","author":"C. Allan","year":"2005","unstructured":"Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhot\u00e1k, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to aspectj. SIGPLAN Not.\u00a040, 345\u2013364 (2005)","journal-title":"SIGPLAN Not."},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Artho, C., Biere, A.: Combined static and dynamic analysis. In: AIOOL 2005. Electr. Notes Theor. Comput. Sci., vol.\u00a0131, pp. 3\u201314 (2005)","DOI":"10.1016\/j.entcs.2005.01.018"},{"issue":"7","key":"24_CR7","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T. Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with slam. Commun. ACM\u00a054(7), 68\u201376 (2011)","journal-title":"Commun. ACM"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-45165-X_2","volume-title":"Java on Smart Cards: Programming and Security","author":"B. Beckert","year":"2001","unstructured":"Beckert, B.: A Dynamic Logic for the Formal Verification of Java Card Programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol.\u00a02041, pp. 6\u201324. Springer, Heidelberg (2001)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-73770-4_12","volume-title":"Tests and Proofs","author":"B. Beckert","year":"2007","unstructured":"Beckert, B., Gladisch, C.: White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol.\u00a04454, pp. 207\u2013216. Springer, Heidelberg (2007)"},{"key":"24_CR11","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/BFb0028771","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: InVeST: A tool for the verification of invariants. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 505\u2013510. Springer, Heidelberg (1998)"},{"issue":"2","key":"24_CR13","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1109\/32.988495","volume":"28","author":"K. Bhargavan","year":"2002","unstructured":"Bhargavan, K., Gunter, C.A., Kim, M., Lee, I., Obradovic, D., Sokolsky, O., Viswanathan, M.: Verisim: Formal analysis of network simulations. IEEE Trans. Software Eng.\u00a028(2), 129\u2013145 (2002)","journal-title":"IEEE Trans. Software Eng."},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-77395-5_3","volume-title":"Runtime Verification","author":"E. Bodden","year":"2007","unstructured":"Bodden, E., Hendren, L.J., Lam, P., Lhot\u00e1k, O., Naeem, N.A.: Collaborative Runtime Verification with Tracematches. In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol.\u00a04839, pp. 22\u201337. Springer, Heidelberg (2007)"},{"issue":"3","key":"24_CR15","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1093\/logcom\/exn077","volume":"20","author":"E. Bodden","year":"2010","unstructured":"Bodden, E., Hendren, L.J., Lam, P., Lhot\u00e1k, O., Naeem, N.A.: Collaborative runtime verification with tracematches. J. Log. Comput.\u00a020(3), 707\u2013723 (2010)","journal-title":"J. Log. Comput."},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-540-73589-2_25","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"E. Bodden","year":"2007","unstructured":"Bodden, E., Hendren, L., Lhot\u00e1k, O.: A Staged Static Program Analysis to Improve the Performance of Runtime Monitoring. In: Bateni, M. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, pp. 525\u2013549. Springer, Heidelberg (2007)"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Bodden, E., Lam, P., Hendren, L.J.: Finding programming errors earlier by evaluating runtime monitors ahead-of-time. In: SIGSOFT FSE 2008, pp. 36\u201347. ACM (2008)","DOI":"10.1145\/1453101.1453109"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-16612-9_15","volume-title":"Runtime Verification","author":"E. Bodden","year":"2010","unstructured":"Bodden, E., Lam, P., Hendren, L.J.: Clara: A Framework for Partially Evaluating Finite-State Runtime Monitors Ahead of Time. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 183\u2013197. Springer, Heidelberg (2010)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11759744_7","volume-title":"Formal Approaches to Software Testing","author":"A.D. Brucker","year":"2006","unstructured":"Brucker, A.D., Wolff, B.: Interactive Testing with HOL-TestGen. In: Grieskamp, W., Weise, C. (eds.) FATES 2005. LNCS, vol.\u00a03997, pp. 87\u2013102. Springer, Heidelberg (2006)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.-L.: Java Applet Correctness: A Developer-Oriented Approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-31980-1_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Chen","year":"2005","unstructured":"Chen, F., Ro\u015fu, G.: Java-MOP: A Monitoring Oriented Programming Environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 546\u2013550. Springer, Heidelberg (2005)"},{"key":"24_CR22","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: SERP 2002, pp. 322\u2013328. CSREA Press (2002)"},{"key":"24_CR23","unstructured":"Colombo, C.: Practical runtime monitoring with impact guarantees of Java programs with real-time constraints. Master\u2019s thesis, University of Malta (2008)"},{"key":"24_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-011-0126-0","volume":"40","author":"C. Colombo","year":"2012","unstructured":"Colombo, C., Pace, G.J., Abela, P.: Safer asynchronous runtime monitoring using compensations. Formal Methods in System Design\u00a040, 1\u201326 (2012)","journal-title":"Formal Methods in System Design"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-03240-0_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"C. Colombo","year":"2009","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol.\u00a05596, pp. 135\u2013149. Springer, Heidelberg (2009)"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: Larva - a tool for runtime monitoring of java programs. In: SEFM 2009, pp. 33\u201337. IEEE Computer Society (2009)","DOI":"10.1109\/SEFM.2009.13"},{"issue":"4","key":"24_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1082983.1083249","volume":"30","author":"M. d\u2019Amorim","year":"2005","unstructured":"d\u2019Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. SIGSOFT Softw. Eng. Notes\u00a030(4), 1\u20137 (2005)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., S\u00e1nchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: Runtime monitoring of synchronous systems. In: TIME 2005, pp. 166\u2013174. IEEE Computer Society Press (June 2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Deng, X., Lee, J., Robby: Bogor\/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In: ASE 2006, pp. 157\u2013166. IEEE Computer Society (2006)","DOI":"10.1109\/ASE.2006.26"},{"key":"24_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-73770-4_10","volume-title":"Tests and Proofs","author":"C. Engel","year":"2007","unstructured":"Engel, C., H\u00e4hnle, R.: Generating Unit Tests from Formal Proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol.\u00a04454, pp. 169\u2013188. Springer, Heidelberg (2007)"},{"issue":"2","key":"24_CR31","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1109\/32.908957","volume":"27","author":"M. Ernst","year":"2001","unstructured":"Ernst, M., Cockrell, J., Griswold, W., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering\u00a027(2), 99\u2013123 (2001)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"24_CR32","unstructured":"Falzon, K.: Combining runtime verification and testing techniques. Master\u2019s thesis, University of Malta (2010)"},{"key":"24_CR33","unstructured":"Goldberg, A., Havelund, K.: Automated runtime verification with eagle. In: MSVVEIS (2005)"},{"key":"24_CR34","doi-asserted-by":"crossref","unstructured":"Grieskamp, W., Tillmann, N., Schulte, W.: XRT \u2014 exploring runtime for.NET architecture and applications. In: Proc. Workshop on Software Model Checking (SoftMC 2005), Edinburgh, UK. Electr. Notes Theor. Comput. Sci, vol.\u00a0144(3), pp. 3\u201326 (2006)","DOI":"10.1016\/j.entcs.2006.01.002"},{"key":"24_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-00768-2_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gupta","year":"2009","unstructured":"Gupta, A., Majumdar, R., Rybalchenko, A.: From Tests to Proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 262\u2013276. Springer, Heidelberg (2009)"},{"key":"24_CR36","first-page":"143","volume-title":"ASE 2010","author":"R. H\u00e4hnle","year":"2010","unstructured":"H\u00e4hnle, R., Baum, M., Bubel, R., Rothe, M.: A visual interactive debugger based on symbolic execution. In: ASE 2010, pp. 143\u2013146. ACM, New York (2010)"},{"issue":"10","key":"24_CR37","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580, 583 (1969)","journal-title":"Commun. ACM"},{"key":"24_CR38","doi-asserted-by":"crossref","unstructured":"Hunt, J.J., Jenn, E., Leriche, S., Schmitt, P., Tonin, I., Wonnemann, C.: A case study of specification and verification using JML in an avionics application. In: JTRES 2006, pp. 107\u2013116. ACM Press (2006)","DOI":"10.1145\/1167999.1168018"},{"key":"24_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-540-27815-3_21","volume-title":"Algebraic Methodology and Software Technology","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B., March\u00e9, C., Rauch, N.: Formal Verification of a Commercial Smart Card Applet with Multiple Tools. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 241\u2013257. Springer, Heidelberg (2004)"},{"issue":"2","key":"24_CR40","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"M. Kim","year":"2004","unstructured":"Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-mac: A run-time assurance approach for java programs. Formal Methods in System Design\u00a024(2), 129\u2013155 (2004)","journal-title":"Formal Methods in System Design"},{"key":"24_CR41","unstructured":"King, J.C.: A program verifier. PhD thesis, Carnegie-Mellon University (1969)"},{"key":"24_CR42","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a java modeling language. In: Formal Underpinnings of Java Workshop, at OOPSLA 1998 (1998)"},{"key":"24_CR43","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual. Draft Revision 1. 200 (2007)"},{"key":"24_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-27705-4_19","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F. Logozzo","year":"2012","unstructured":"Logozzo, F.: Our Experience with the CodeContracts Static Checker. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 241\u2013242. Springer, Heidelberg (2012)"},{"issue":"2","key":"24_CR45","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10515-010-0063-y","volume":"17","author":"P.O. Meredith","year":"2010","unstructured":"Meredith, P.O., Jin, D., Chen, F., Rosu, G.: Efficient monitoring of parametric context-free patterns. Autom. Softw. Eng.\u00a017(2), 149\u2013180 (2010)","journal-title":"Autom. Softw. Eng."},{"key":"24_CR46","unstructured":"Meyer, B.: Design by Contract. Technical Report TR-EI-12\/CO, Interactive Software Engineering Inc. (1986)"},{"key":"24_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-540-31984-9_27","volume-title":"Fundamental Approaches to Software Engineering","author":"W. Mostowski","year":"2005","unstructured":"Mostowski, W.: Formalisation and Verification of Java Card Security Properties in Dynamic Logic. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 357\u2013371. Springer, Heidelberg (2005)"},{"key":"24_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-642-00255-7_20","volume-title":"Integrated Formal Methods","author":"G.J. Pace","year":"2009","unstructured":"Pace, G.J., Schneider, G.: Challenges in the Specification of Full Contracts. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol.\u00a05423, pp. 292\u2013306. Springer, Heidelberg (2009)"},{"issue":"4","key":"24_CR49","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1016\/j.jlap.2012.03.003","volume":"81","author":"C. Prisacariu","year":"2012","unstructured":"Prisacariu, C., Schneider, G.: A dynamic deontic logic for complex contracts. J. Log. Algebr. Program\u00a081(4), 458\u2013490 (2012)","journal-title":"J. Log. Algebr. Program"},{"key":"24_CR50","unstructured":"R\u00fcmmer, P.: Generating counterexamples for Java Dynamic logic. In: Prel. Proc. of Workshop on Disproving at CADE 2005, pp. 32\u201344 (2005)"},{"key":"24_CR51","doi-asserted-by":"crossref","unstructured":"Schmitt, P.H., Tonin, I.: Verifying the Mondex case study. In: SEFM 2007, pp. 47\u201356. IEEE Press (2007)","DOI":"10.1109\/SEFM.2007.47"},{"key":"24_CR52","unstructured":"Stenzel, K.: Verification of Java Card Programs. PhD thesis, Fakult\u00e4t f\u00fcr angewandte Informatik, University of Augsburg (2005)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34026-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:24:12Z","timestamp":1744205052000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34026-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340253","9783642340260"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34026-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}