{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:00:13Z","timestamp":1725494413659},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_21","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T07:58:07Z","timestamp":1194854287000},"page":"283-298","source":"Crossref","is-referenced-by-count":11,"title":["Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Logozzo","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"JUnit: http:\/\/junit.sourceforge.net\/"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Aggarwal, A., Randall, K.H: Related field analysis. In: PLDI (2001)","DOI":"10.1145\/378795.378850"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","first-page":"10","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., et al. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 10\u201314. Springer, Heidelberg (2005)"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Escape Analysis: Correctness proof, implementation and experimental results. In: POPL (1998)","DOI":"10.1145\/268946.268949"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Cok, D.R, Kiniry, J.: ESC\/Java 2: Uniting ESC\/Java and JML. In: CASSIS (2004)","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation, 2(4) (August 1992)","DOI":"10.1093\/logcom\/2.4.511"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Ernst, M.D: Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington (2000)","DOI":"10.1145\/302405.302467"},{"key":"21_CR9","unstructured":"Ferrara, P.: JAIL: Firewall analysis of JavaCard by Abstract Interpretation. In: EAAI (2006)"},{"key":"21_CR10","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. Sun Microsystems (2001)"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"J. Henkel","year":"2003","unstructured":"Henkel, J., Diwan, A.: Discovering algebraic specifications from java classes. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, Springer, Heidelberg (2003)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Jacobs, B., van den Berg, J., Huismann, H., van Berkum, M., Hensel, U., Tews, H. Reasoning about Java classes (preliminary report). In: OOPSLA (1998)","DOI":"10.1145\/286936.286973"},{"key":"21_CR13","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary Design of JML: A Behavioral Interface Specification Language for Java (November 2003)"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Algebraic Methodology and Software Technology","author":"F. Logozzo","year":"2004","unstructured":"Logozzo, F.: Separate compositional analysis of class-based object-oriented languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, Springer, Heidelberg (2004)"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Logozzo, F.: Modular Static Analysis of Object-oriented languages. PhD thesis, \u00c9cole Polytecnique (2004)","DOI":"10.1007\/3-540-44898-5_3"},{"key":"21_CR16","unstructured":"Logozzo, F.: Class invariants as abstract interpretation of trace semantics. Computer Languages, Systems and Structures (2007)"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java\/Javacard programs. Annotated in JML. J. Log. Algebr. Program, 58(1\u20132) (2004)","DOI":"10.1016\/j.jlap.2003.07.006"},{"key":"21_CR18","volume-title":"Professional Technical Reference","author":"B. Meyer.","year":"1997","unstructured":"Meyer., B.: Object-Oriented Software Construction. In: Professional Technical Reference, 2nd edn., Prentice Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"21_CR19","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: AST (2001)"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_5","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"I. Pollet","year":"2001","unstructured":"Pollet, I., Le Charlier, B., Cortesi, A.: Distinctness and sharing domains for static analysis of Java programs. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, Springer, Heidelberg (2001)"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Rossignoli","year":"2005","unstructured":"Rossignoli, S., Spoto, F.: Detecting Non-Cyclicity by Abstract Compilation into Boolean Functions. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, Springer, Heidelberg (2005)"},{"key":"21_CR22","unstructured":"Spoto, F.: Julia: A generic static analyser for the java bytecode. In: FTfJP (2005)"},{"key":"21_CR23","unstructured":"Everest Team: Jack, Java Applet Correctness Kit, http:\/\/www-sop.inria.fr\/everest\/soft\/Jack\/jack.html"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Tillmann, N., Chen, F., Schulte, W.: Discovering likely method specifications. Technical report, Microsoft Research (2006)","DOI":"10.1007\/11901433_39"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:45:07Z","timestamp":1620002707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_21","relation":{},"subject":[]}}