{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T16:06:55Z","timestamp":1764259615588,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540773948"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77395-5_17","type":"book-chapter","created":{"date-parts":[[2007,12,6]],"date-time":"2007-12-06T11:25:53Z","timestamp":1196940353000},"page":"202-213","source":"Crossref","is-referenced-by-count":10,"title":["Runtime Checking for Program Verification"],"prefix":"10.1007","author":[{"given":"Karen","family":"Zee","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Taylor","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhotak, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: Proc. 20th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 345\u2013364 (2005)","DOI":"10.1145\/1094811.1094839"},{"key":"17_CR2","unstructured":"Arkoudas, K., Rinard, M.: Deductive runtime certification. In: RV 2004. Proceedings of the 2004 Workshop on Runtime Verification, Barcelona, Spain (April 2004)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS: Int. Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices (2004)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Bartetzko, D., Fischer, C., M\u00f6ller, M., Wehrheim, H.: Jass\u2013Java with assertions. In: RV 2001. ENTCS, vol.\u00a055, pp. 103\u2013117 (2001)","DOI":"10.1016\/S1571-0661(04)00247-6"},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/582353.582361","volume-title":"Proceedings of the 1982 ACM SIGMOD international conference on Management of data","author":"P.A. Bernstein","year":"1982","unstructured":"Bernstein, P.A., Blaustein, B.T.: Fast methods for testing quantified relational calculus assertions. In: Proceedings of the 1982 ACM SIGMOD international conference on Management of data, pp. 39\u201350. ACM Press, New York (1982)"},{"issue":"2","key":"17_CR7","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1109\/TSE.2005.23","volume":"31","author":"D. Beyer","year":"2005","unstructured":"Beyer, D., Noack, A., Lewerentz, C.: Efficient relational calculation for software analysis. IEEE Trans. Software Eng.\u00a031(2), 137\u2013149 (2005)","journal-title":"IEEE Trans. Software Eng."},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C. Bouillaguet","year":"2007","unstructured":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: Using first-order theorem provers in a data structure verification system. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, Springer, Heidelberg (2007)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: Proc. International Symposium on Software Testing and Analysis, pp. 123\u2013133 (July 2002)","DOI":"10.1145\/566171.566191"},{"issue":"4","key":"17_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2006.02.002","volume":"144","author":"F. Chen","year":"2006","unstructured":"Chen, F., d\u2019Amorim, M., Rosu, G.: Checking and correcting behaviors of java programs at runtime with java-mop. Electr. Notes Theor. Comput. Sci.\u00a0144(4), 3\u201320 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Chen, F., Ro\u015fu, G.: MOP: An Efficient and Generic Runtime Verification Framework. In: OOPSLA 2007. Object-Oriented Programming, Systems, Languages and Applications (2007)","DOI":"10.1145\/1297027.1297069"},{"key":"17_CR12","unstructured":"Cheon, Y.: A Runtime Assertion Checker for the Java Modeling Language. PhD thesis, Iowa State University, April (2003)"},{"issue":"3","key":"17_CR13","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/1127878.1127900","volume":"31","author":"L.A. Clarke","year":"2006","unstructured":"Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes\u00a031(3), 25\u201337 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Cok, D.R., Kiniry, J.R.: Esc\/java2: Uniting ESC\/Java and JML. In: CASSIS: Construction and Analysis of Safe, Secure and Interoperable Smart devices (2004)","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Demsky, B., Cadar, C., Roy, D., Rinard, M.C.: Efficient specification-assisted error localization. In: Second International Workshop on Dynamic Analysis (2004)","DOI":"10.1049\/ic:20040301"},{"key":"17_CR16","volume-title":"Finite Model Theory","author":"H.D. Ebbinghaus","year":"1995","unstructured":"Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Springer, Heidelberg (1995)"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Flanagan, C.: Hybrid type checking. In: POPL, pp. 245\u2013256 (2006)","DOI":"10.1145\/1111320.1111059"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lilibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: ACM Conf. Programming Language Design and Implementation (PLDI) (2002)","DOI":"10.1145\/512557.512558"},{"issue":"3","key":"17_CR19","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1109\/69.599937","volume":"9","author":"T. Griffin","year":"1997","unstructured":"Griffin, T., Libkin, L., Trickey, H.: An improved algorithm for incremental recomputation of active relational expressions. IEEE Transactions on Knowledge and Data Engineering\u00a09(3), 508\u2013511 (1997)","journal-title":"IEEE Transactions on Knowledge and Data Engineering"},{"key":"17_CR20","unstructured":"Henschen, L.J., McCune, W., Naqvi, S.A.: Compiling constraint-checking programs from first-order formulas. In: Gallaire, H., Nicolas, J.-M., Minker, J. (eds.) Advances in Data Base Theory, Proceedings of the Workshop on Logical Data Bases, 2nd edn, pp. 145\u2013169 (1984). ISBN 0-306-41636-0."},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/BFb0029359","volume-title":"Proc. Intl. Sym. on Operating Systems","author":"J.J. Horning","year":"1974","unstructured":"Horning, J.J., Lauer, H.C., Melliar-Smith, P.M., Randell, B.: A program structure for error detection and recovery. In: Gelenbe, E., Kaiser, C. (eds.) Operating Systems. LNCS, vol.\u00a016, pp. 171\u2013187. Springer, Heidelberg (1974)"},{"key":"17_CR22","volume-title":"Descriptive Complexity","author":"N. Immerman","year":"1998","unstructured":"Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1998)"},{"key":"17_CR23","volume-title":"Software Abstractions: Logic, Language, & Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, & Analysis. MIT Press, Cambridge (2006)"},{"key":"17_CR24","volume-title":"Proceedings of the 18th Conference on Very Large Databases","author":"H.V. Jagadish","year":"1992","unstructured":"Jagadish, H.V., Qian, X.: Integrity maintenance in object-oriented databases. In: Proceedings of the 18th Conference on Very Large Databases, Los Altos CA, Vancouver, Morgan Kaufmann pubs, San Francisco (1992)"},{"key":"17_CR25","first-page":"1","volume-title":"Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 1\u201333. IEEE Computer Society Press, Washington (1990)"},{"issue":"4","key":"17_CR26","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1023\/B:AUSE.0000038938.10589.b9","volume":"11","author":"S. Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D.: TestEra: Specification-based testing of java programs using SAT. Autom. Softw. Eng.\u00a011(4), 403\u2013434 (2004)","journal-title":"Autom. Softw. Eng."},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. 5th International Conference on Implementation and Application of Automata","author":"N. Klarlund","year":"2000","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Wilhelm, R. (ed.) Proc. 5th International Conference on Implementation and Application of Automata. LNCS, Springer, Heidelberg (2000)"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-70952-7_19","volume-title":"Formal Methods: Applications and Technology","author":"B. Krause","year":"2007","unstructured":"Krause, B., Wahls, T.: jmle: A tool for executing JML specifications via constraint programming. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 293\u2013296. Springer, Heidelberg (2007)"},{"key":"17_CR29","unstructured":"Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean Algebra with Presburger Arithmetic. In: J. of Automated Reasoning (2006), http:\/\/dx.doi.org\/10.1007\/s10817-006-9042-1 .","DOI":"10.1007\/s10817-006-9042-1"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: An overview of the Jahob analysis system: Project goals and current status. In: NSF Next Generation Software Workshop (2006)","DOI":"10.1109\/IPDPS.2006.1639580"},{"key":"17_CR32","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for boolean algebra with presburger arithmetic. In: Conference on Automateded Deduction (CADE-21) (2007)"},{"key":"17_CR33","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual. February (2007)"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Martin, M., Livshits, B., Lam, M.S.: Finding application errors and security flaws using PQL: a Program Query Language. In: Proc. 20th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (2005)","DOI":"10.1145\/1094811.1094840"},{"key":"17_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. In: Isabelle\/HOL. LNCS, vol.\u00a02283, Springer, Heidelberg (2002)"},{"key":"17_CR36","unstructured":"Paige, R.: Applications of finite differencing to database integrity control and query\/transaction optimization. In: Gallaire, H., Nicolas, J.-M., Minker, J. (eds.) Advances in Data Base Theory, Proceedings of the Workshop on Logical Data Bases, 2nd edn, pp. 171\u2013209 (1984). ISBN 0-306-41636-0."},{"key":"17_CR37","first-page":"3","volume-title":"VLDB 1986 Twelfth International Conference on Very Large Data Bases, August 25-28, 1986, Kyoto, Japan, Proceedings","author":"X. Qian","year":"1986","unstructured":"Qian, X., Wiederhold, G.: Knowledge-based integrity constraint validation. In: Chu, W.W., Gardarin, G., Ohsuga, S., Kambayashi, Y. (eds.) VLDB 1986 Twelfth International Conference on Very Large Data Bases, August 25-28, 1986, Kyoto, Japan, Proceedings, pp. 3\u201312. Morgan Kaufmann, San Francisco (1986)"},{"issue":"2\/3","key":"17_CR38","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. Journal of AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"key":"17_CR39","doi-asserted-by":"crossref","unstructured":"Shankar, A., Bodik, R.: Ditto: Automatic incrementalization of data structure invariant checks. In: PLDI (2007)","DOI":"10.1145\/1250734.1250770"},{"key":"17_CR40","doi-asserted-by":"crossref","unstructured":"Stolz, V., Bodden, E.: Temporal assertions using AspectJ (2005)","DOI":"10.1016\/j.entcs.2006.02.007"},{"key":"17_CR41","series-title":"Lecture Notes in Computer Science","volume-title":"TACAS 2007","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, Springer, Heidelberg (2007)"},{"key":"17_CR42","doi-asserted-by":"crossref","unstructured":"Wies, T., Kuncak, V., Lam, P., Podelski, A., Rinard, M.: Field constraint analysis. In: Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation (2006)","DOI":"10.1007\/11609773_11"},{"key":"17_CR43","unstructured":"Wies, T., Kuncak, V., Zee, K., Podelski, A., Rinard, M.: Verifying complex properties using symbolic shape analysis. In: Workshop on Heap Abstraction and Verification (collocated with ETAPS) (2007)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77395-5_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:10:33Z","timestamp":1619521833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77395-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540773948"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77395-5_17","relation":{},"subject":[]}}