{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:12:34Z","timestamp":1725901954911},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540737698"},{"type":"electronic","value":"9783540737704"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73770-4_3","type":"book-chapter","created":{"date-parts":[[2007,8,24]],"date-time":"2007-08-24T16:00:13Z","timestamp":1187971213000},"page":"41-60","source":"Crossref","is-referenced-by-count":9,"title":["Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic"],"prefix":"10.1007","author":[{"given":"Philipp","family":"R\u00fcmmer","sequence":"first","affiliation":[]},{"given":"Muhammad Ali","family":"Shah","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"3_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software","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":"3_CR3","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C.: JML Reference Manual (August 2002)"},{"key":"3_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/11916277_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2006","unstructured":"R\u00fcmmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 422\u2013436. Springer, Heidelberg (2006)"},{"issue":"7","key":"3_CR5","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Communications of the ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Communications of the ACM"},{"issue":"9","key":"3_CR6","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/357766.351266","volume":"35","author":"K. Claessen","year":"2000","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices\u00a035(9), 268\u2013279 (2000)","journal-title":"ACM SIGPLAN Notices"},{"key":"3_CR7","unstructured":"Edvardsson, J.: A survey on automatic test data generation. In: ECSEL. Proceedings of the Second Conference on Computer Science and Engineering in Linkping, pp. 21\u201328 (October 1999)"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/B978-044450813-3\/50005-9","volume-title":"Handbook of Automated Reasoning","author":"R. H\u00e4hnle","year":"2001","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, pp. 101\u2013178. Elsevier Science BV, Amsterdam (2001)"},{"key":"3_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M.C. Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, New York (1996)","edition":"2"},{"key":"3_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-45744-5_46","volume-title":"Automated Reasoning","author":"M. Giese","year":"2001","unstructured":"Giese, M.: Incremental closure of free variable tableaux. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 545\u2013560. Springer, Heidelberg (2001)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 553\u2013568. Springer, Heidelberg (2003)"},{"issue":"3","key":"3_CR12","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/125826.125848","volume-title":"Supercomputing 1991","author":"W. Pugh","year":"1991","unstructured":"Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Supercomputing 1991. Proceedings of the 1991 ACM\/IEEE conference on Supercomputing, pp. 4\u201313. ACM Press, New York, USA (1991)"},{"issue":"4","key":"3_CR14","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on common lisp. IEEE Trans. Softw. Eng.\u00a023(4), 203\u2013213 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/288195.288321","volume-title":"SIGSOFT 1998\/FSE-6","author":"N. Gupta","year":"1998","unstructured":"Gupta, N., Mathur, A.P., Soffa, M.L.: Automated test data generation using an iterative relaxation method. In: SIGSOFT 1998\/FSE-6. Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 231\u2013244. ACM Press, New York (1998)"},{"issue":"4","key":"3_CR16","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer\u00a02(4), 410\u2013425 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"3_CR17","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering\u00a010(2), 203\u2013232 (2003)","journal-title":"Automated Software Engineering"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings PLDI, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: Proceedings PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"3_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1007\/3-540-45744-5_52","volume-title":"Automated Reasoning","author":"W. Reif","year":"2001","unstructured":"Reif, W., Schellhorn, G., Thums, A.: Flaw detection in formal specifications. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 642\u2013657. Springer, Heidelberg (2001)"},{"key":"3_CR22","unstructured":"Shah, M.A.: Generating counterexamples for Java dynamic logic. Master\u2019s thesis (November 2005)"},{"key":"3_CR23","unstructured":"Parasoft: JTest (2006), \n                  \n                    http:\/\/www.parasoft.com\/jsp\/products\/home.jsp?product=Jtest"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73770-4_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:58:36Z","timestamp":1619517516000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73770-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540737698","9783540737704"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73770-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}