{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T23:59:58Z","timestamp":1740095998501,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642029585"},{"type":"electronic","value":"9783642029592"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_1","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T01:02:22Z","timestamp":1248483742000},"page":"1-16","source":"Crossref","is-referenced-by-count":5,"title":["Integrated Reasoning and Proof Choice Point Selection in the Jahob System \u2013 Mechanisms for Program Survival"],"prefix":"10.1007","author":[{"given":"Martin","family":"Rinard","sequence":"first","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Demsky, B., Rinard, M.: Data structure repair using goal-directed reasoning. In: Proceedings of the 2005 International Conference on Software Engineering (2005)","key":"1_CR1","DOI":"10.1145\/1062455.1062499"},{"doi-asserted-by":"crossref","unstructured":"Rinard, M.: Acceptability-oriented computing. In: 2003 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications Companion (OOPSLA 2003 Companion) Onwards! Session (October 2003)","key":"1_CR2","DOI":"10.1145\/949344.949402"},{"doi-asserted-by":"crossref","unstructured":"Rinard, M., Cadar, C., Nguyen, H.H.: Exploring the acceptability envelope. In: 2005 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications Companion (OOPSLA 2005 Companion) Onwards! Session (October 2005)","key":"1_CR3","DOI":"10.1145\/1094855.1094866"},{"unstructured":"Rinard, M., Cadar, C., Dumitran, D., Roy, D.M., Leu, T., William, S., Beebee, J.: Enhancing server availability and security through failure-oblivious computing. In: Proceeding of 6th Symposium on Operating System Design and Implementation (OSDI 2004) (2004)","key":"1_CR4"},{"doi-asserted-by":"crossref","unstructured":"Rinard, M., Cadar, C., Dumitran, D., Roy, D.M., Leu, T.: A dynamic technique for eliminating buffer overflow vulnerabilities (and other memory errors). In: Proceedings of the 2004 Annual Computer Security Applications Conference (2004)","key":"1_CR5","DOI":"10.1109\/CSAC.2004.2"},{"doi-asserted-by":"crossref","unstructured":"Demsky, B., Rinard, M.: Automatic detection and repair of errors in data structures. In: Proc. 18th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (2003)","key":"1_CR6","DOI":"10.1145\/949305.949314"},{"doi-asserted-by":"crossref","unstructured":"Demsky, B., Rinard, M.: Static specification analysis for termination of specification-based data structure repair. In: IEEE International Symposium on Software Reliability (2003)","key":"1_CR7","DOI":"10.1109\/ISSRE.2003.1251032"},{"doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008) (June 2008)","key":"1_CR8","DOI":"10.1145\/1375581.1375624"},{"doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: An integrated proof language for imperative programs. In: Proceedings of the ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation (PLDI 2009) (June 2009)","key":"1_CR9","DOI":"10.1145\/1542476.1542514"},{"unstructured":"Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)","key":"1_CR10"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0II, pp. 1965\u20132013. Elsevier Science, Amsterdam (2001)"},{"issue":"2\/3","key":"1_CR12","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":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-73595-3_12","volume-title":"Automated Deduction \u2013 CADE-21","author":"Y. Ge","year":"2007","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 167\u2013182. Springer, Heidelberg (2007)"},{"key":"1_CR15","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.M. Moura de","year":"2008","unstructured":"de Moura, L.M., 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":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L. Moura de","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Henriksen","year":"1995","unstructured":"Henriksen, J., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019. Springer, Heidelberg (1995)"},{"unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical report, Department of Computer Science, The University of Iowa (2006), www.SMT-LIB.org","key":"1_CR18"},{"doi-asserted-by":"crossref","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean Algebra with Presburger Arithmetic. J. of Automated Reasoning (2006), http:\/\/dx.doi.org\/10.1007\/s10817-006-9042-1","key":"1_CR19","DOI":"10.1007\/s10817-006-9042-1"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-73595-3_15","volume-title":"Automated Deduction \u2013 CADE-21","author":"V. Kuncak","year":"2007","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 215\u2013230. Springer, Heidelberg (2007)"},{"key":"1_CR21","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. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"1_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development\u2013Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development\u2013Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Witchel, E., Rhee, J., Asanovi\u0107, K.: Mondrix: Memory isolation for linux using mondriaan memory protection. In: 20th ACM Symposium on Operating Systems Principles (SOSP-20) (2005)","key":"1_CR23","DOI":"10.1145\/1095810.1095814"},{"doi-asserted-by":"crossref","unstructured":"Nguyen, H.H., Rinard, M.: Detecting and eliminating memory leaks using cyclic memory allocation. In: Proceedings of the 2007 International Symposium on Memory Management (2007)","key":"1_CR24","DOI":"10.1145\/1296907.1296912"},{"doi-asserted-by":"crossref","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Cross-cutting techniques in program specification and analysis. In: 4th International Conference on Aspect-Oriented Software Development (AOSD 2005) (2005)","key":"1_CR25","DOI":"10.1145\/1052898.1052913"},{"doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Zee, K., Rinard, M.: Modular pluggable analyses for data structure consistency. IEEE Transactions on Software Engineering\u00a032(12) (December 2006)","key":"1_CR26","DOI":"10.1109\/TSE.2006.125"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-540-30579-8_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Lam","year":"2005","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking for data structure consistency. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 430\u2013447. Springer, Heidelberg (2005)"},{"unstructured":"Lam, P.: The Hob System for Verifying Software Design Properties. PhD thesis, Massachusetts Institute of Technology (February 2007)","key":"1_CR28"},{"doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (PLDI 2006) (June 2006)","key":"1_CR29","DOI":"10.1145\/1133981.1134029"},{"doi-asserted-by":"crossref","unstructured":"Papi, M.M., Ali, M., Correa Jr., T.L., Perkins, J.H., Ernst, M.D.: Practical pluggable types for java. In: Proceedings of the 2008 International Symposium on Software Testing and Analysis, Seattle, WA (July 2008)","key":"1_CR30","DOI":"10.1145\/1390630.1390656"},{"doi-asserted-by":"crossref","unstructured":"Rugina, R., Rinard, M.C.: Symbolic bounds analysis of pointers, array indices, and accessed memory regions. ACM Trans. Program. Lang. Syst.\u00a027(2) (2005)","key":"1_CR31","DOI":"10.1145\/1057387.1057388"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-46423-9_4","volume-title":"Compiler Construction","author":"R. Shaham","year":"2000","unstructured":"Shaham, R., Kolodner, E., Sagiv, S.: Automatic removal of array memory leaks in java. In: Watt, D.A. (ed.) CC 2000. LNCS, vol.\u00a01781, p. 50. Springer, Heidelberg (2000)"},{"doi-asserted-by":"crossref","unstructured":"Whaley, J., Rinard, M.: Compositional pointer and escape analysis for Java programs. In: OOPSLA, Denver (November 1999)","key":"1_CR33","DOI":"10.1145\/320384.320400"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T13:52:02Z","timestamp":1558446722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}