{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:48:47Z","timestamp":1725792527681},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319061993"},{"type":"electronic","value":"9783319062006"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06200-6_13","type":"book-chapter","created":{"date-parts":[[2014,4,23]],"date-time":"2014-04-23T05:53:48Z","timestamp":1398232428000},"page":"173-187","source":"Crossref","is-referenced-by-count":3,"title":["JKelloy: A Proof Assistant for Relational Specifications of Java Programs"],"prefix":"10.1007","author":[{"given":"Aboubakr Achraf","family":"El Ghazi","sequence":"first","affiliation":[]},{"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Gladisch","sequence":"additional","affiliation":[]},{"given":"Shmuel","family":"Tyszberowicz","sequence":"additional","affiliation":[]},{"given":"Mana","family":"Taghdiri","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-88194-0_14","volume-title":"Formal Methods and Software Engineering","author":"N.M. Aguirre","year":"2008","unstructured":"Aguirre, N.M., Frias, M.F., Ponzio, P., Cardiff, B.J., Galeotti, J.P., Regis, G.: Towards abstraction for DynAlloy specifications. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 207\u2013225. Springer, Heidelberg (2008)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-24771-5_3","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"K. Arkoudas","year":"2004","unstructured":"Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating model checking and theorem proving for relational reasoning. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol.\u00a03051, pp. 21\u201333. Springer, Heidelberg (2004)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. Springer (2007)","DOI":"10.1007\/978-3-540-69061-0"},{"issue":"8","key":"13_CR4","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a SAT solver. In: FSE, pp. 195\u2013204 (2007)","DOI":"10.1145\/1287624.1287653"},{"key":"13_CR6","unstructured":"El Ghazi, A.A., Ulbrich, M., Gladisch, C., Tyszberowicz, S., Taghdiri, M.: On verifying relational specifications of Java programs with JKelloy. Technical Report 2014-03, KIT, Department of Informatics (2014)"},{"key":"13_CR7","unstructured":"Galeotti, J.P.: Software Verification using Alloy. PhD thesis, Universidad de Buenos Aires (2010)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-41071-0_8","volume-title":"Formal Methods: Foundations and Applications","author":"C. Gladisch","year":"2013","unstructured":"Gladisch, C., Tyszberowicz, S.: Specifying a linked data structure in JML for formal verification and runtime checking. In: Iyoda, J., de Moura, L. (eds.) SBMF 2013. LNCS, vol.\u00a08195, pp. 99\u2013114. Springer, Heidelberg (2013)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"13_CR10","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2012)"},{"issue":"7","key":"13_CR11","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"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: Proceedings of POPL, pp. 115\u2013126. ACM (2006)","DOI":"10.1145\/1111320.1111048"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science\u00a05(2) (2009)","DOI":"10.2168\/LMCS-5(2:12)2009"},{"issue":"10","key":"13_CR14","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE Computer\u00a025(10), 40\u201351 (1992)","journal-title":"IEEE Computer"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-14808-8_19","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"M.M. Moscato","year":"2010","unstructured":"Moscato, M.M., L\u00f3pez Pombo, C.G., Frias, M.F.: Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol.\u00a06255, pp. 275\u2013289. Springer, Heidelberg (2010)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-540-69738-1_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z. Rakamari\u0107","year":"2007","unstructured":"Rakamari\u0107, Z., Bingham, J.D., Hu, A.J.: An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 106\u2013121. Springer, Heidelberg (2007)"},{"key":"13_CR17","unstructured":"Taghdiri, M.: Automating Modular Program Verification by Refining Specifications. PhD thesis. MIT (2008)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-642-28756-5_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Ulbrich","year":"2012","unstructured":"Ulbrich, M., Geilmann, U., El Ghazi, A.A., Taghdiri, M.: A proof assistant for Alloy specifications. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 422\u2013436. Springer, Heidelberg (2012)"},{"key":"13_CR19","unstructured":"Vaziri, M.: Finding Bugs in Software with Constraint Solver. PhD thesis. MIT (2004)"},{"key":"13_CR20","unstructured":"Wei\u00df, B.: Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. PhD thesis. KIT (2010)"},{"key":"13_CR21","unstructured":"Yessenov, K.T.: A Lightweight Specification Language for Bounded Program Verification. Master\u2019s thesis. MIT (2009)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI, pp. 349\u2013361 (2008)","DOI":"10.1145\/1379022.1375624"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06200-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T17:25:57Z","timestamp":1558891557000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06200-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319061993","9783319062006"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06200-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}