{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:31Z","timestamp":1740107971733,"version":"3.37.3"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2015,4,5]],"date-time":"2015-04-05T00:00:00Z","timestamp":1428192000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,11]]},"DOI":"10.1007\/s10009-015-0375-0","type":"journal-article","created":{"date-parts":[[2015,4,4]],"date-time":"2015-04-04T09:32:57Z","timestamp":1428139977000},"page":"653-684","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Provably correct control flow graphs from Java bytecode programs with exceptions"],"prefix":"10.1007","volume":"18","author":[{"given":"Afshin","family":"Amighi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pedro de Carvalho","family":"Gomes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,5]]},"reference":[{"key":"375_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/390013.808479","volume":"5","author":"FE Allen","year":"1970","unstructured":"Allen, F.E.: Control flow analysis. SIGPLAN Not. 5, 1\u201319 (1970). doi: 10.1145\/390013.808479","journal-title":"SIGPLAN Not."},{"unstructured":"Amighi, A.: Flow graph extraction for modular verification of java programs. Master\u2019s thesis, KTH Royal Institute of Technology, Stockholm, Sweden (2011). http:\/\/www.nada.kth.se\/utbildning\/grukth\/exjobb\/rapportlistor\/2011\/rapporter11\/amighi_afshin_11038.pdf . Ref.: TRITA-CSC-E 2011:038","key":"375_CR2"},{"doi-asserted-by":"publisher","unstructured":"Amighi, A., Gomes, PdC, Gurov, D., Huisman, M.: Sound control-flow graph extraction for Java programs with exceptions. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) Software Engineering and Formal Methods, Lecture Notes in Computer Science, vol. 7504, pp. 33\u201347. Springer, Berlin (2012). doi: 10.1007\/978-3-642-33826-7_3","key":"375_CR3","DOI":"10.1007\/978-3-642-33826-7_3"},{"doi-asserted-by":"publisher","unstructured":"Armando, A., Costa, G., Merlo, A., Verderame, L.: Enabling byod through secure meta-market. In: Proceedings of the 2014 ACM Conference on Security and Privacy in Wireless & #38; Mobile Networks, WiSec \u201914, pp. 219\u2013230. ACM, New York (2014). doi: 10.1145\/2627393.2627410 . http:\/\/doi.acm.org\/","key":"375_CR4","DOI":"10.1145\/2627393.2627410"},{"doi-asserted-by":"crossref","unstructured":"Bacon, D.F., Sweeney, P.F.: Fast static analysis of C++ virtual function calls. In: OOPSLA, pp. 324\u2013341 (1996)","key":"375_CR5","DOI":"10.1145\/236337.236371"},{"unstructured":"Barre, N., Demange, D., Hubert, L., Monfort, V., Pichardie, D.: SAWJA API documentation (2011). http:\/\/javalib.gforge.inria.fr\/doc\/sawja-api\/sawja-1.3-doc\/api\/index.html","key":"375_CR6"},{"doi-asserted-by":"crossref","unstructured":"Burke, M.G., Choi, J.D., Fink, S., Grove, D., Hind, M., Sarkar, V., Serrano, M.J., Sreedhar, V.C., Srinivasan, H., Whaley, J.: The Jalape\u00f1o dynamic optimizing compiler for Java. In: Proceedings of the ACM 1999 Conference on Java Grande. JAVA \u201999, pp. 129\u2013141. ACM, New York (1999)","key":"375_CR7","DOI":"10.1145\/304065.304113"},{"key":"375_CR8","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/381788.316171","volume":"24","author":"JD Choi","year":"1999","unstructured":"Choi, J.D., Grove, D., Hind, M., Sarkar, V.: Efficient and precise modeling of exceptions for the analysis of Java programs. SIGSOFT Softw. Eng. Notes 24, 21\u201331 (1999)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"doi-asserted-by":"publisher","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Z.H.: Bandera: extracting finite-state models from java source code. In: Proceedings of the 22nd International Conference on Software Engineering, ICSE \u201900, pp. 439\u2013448. ACM, New York (2000). doi: 10.1145\/337180.337234 . http:\/\/doi.acm.org\/","key":"375_CR9","DOI":"10.1145\/337180.337234"},{"doi-asserted-by":"crossref","unstructured":"Dean, J., Grove, D., Chambers, C.: Optimization of object-oriented programs using static class hierarchy analysis. In: Proceedings of the 9th European Conference on Object-Oriented Programming, ECOOP, pp. 77\u2013101. Springer, London (1995). http:\/\/dl.acm.org\/citation.cfm?id=646153.679523","key":"375_CR10","DOI":"10.1007\/3-540-49538-X_5"},{"unstructured":"Demange, D., Jensen, T., Pichardie, D.: A provably correct stackless intermediate representation for Java bytecode. Tech. Rep. 7021, INRIA Rennes (2009). http:\/\/www.irisa.fr\/celtique\/demange\/bir\/rr7021-3.pdf Version 3, November 2010","key":"375_CR11"},{"doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Hatcliff, J., Joehanes, R., Laubach, S., P\u0103s\u0103reanu, C.S., Zheng, H., Visser, W.: Tool-supported program abstraction for finite-state verification. In: Proceedings of the 23rd International Conference on Software Engineering, ICSE \u201901, pp. 177\u2013187. IEEE Computer Society, Washington, DC (2001). http:\/\/dl.acm.org\/citation.cfm?id=381473.381493","key":"375_CR12","DOI":"10.1109\/ICSE.2001.919092"},{"key":"375_CR13","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1023\/A:1025011624925","volume":"30","author":"SN Freund","year":"2003","unstructured":"Freund, S.N., Mitchell, J.C.: A type system for the Java bytecode language and verifier. J. Autom. Reason. 30, 271\u2013321 (2003)","journal-title":"J. Autom. Reason."},{"unstructured":"Gomes, P.D.C.: Sound modular extraction of control flow graphs from java bytecode. Licentiate Thesis, KTH Royal Institute of Technology (2012). http:\/\/urn.kb.se\/resolve?urn=urn:nbn:se:kth:diva-105275 QC 20121122","key":"375_CR14"},{"unstructured":"Gomes, P.D.C., Picoco, A., Amighi, A.: ConFlEx (2012). http:\/\/www.csc.kth.se\/pedrodcg\/conflex","key":"375_CR15"},{"doi-asserted-by":"publisher","unstructured":"Gomes, PdC, Picoco, A., Gurov, D.: Sound control flow graph extraction from incomplete java bytecode programs. In: Gnesi, S., Rensink, A. (eds.) Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 8411, pp. 215\u2013229. Springer, Berlin (2014). doi: 10.1007\/978-3-642-54804-8_15","key":"375_CR16","DOI":"10.1007\/978-3-642-54804-8_15"},{"doi-asserted-by":"publisher","unstructured":"Graa, M., Cuppens-Boulahia, N., Cuppens, F., Cavalli, A.: Formal characterization of illegal control flow in android system. In: 2013 International Conference on Signal-Image Technology Internet-Based Systems (SITIS), pp. 293\u2013300 (2013). doi: 10.1109\/SITIS.2013.56","key":"375_CR17","DOI":"10.1109\/SITIS.2013.56"},{"issue":"7","key":"375_CR18","doi-asserted-by":"crossref","first-page":"840","DOI":"10.1016\/j.ic.2008.03.003","volume":"206","author":"D Gurov","year":"2008","unstructured":"Gurov, D., Huisman, M., Sprenger, C.: Compositional verification of sequential programs with procedures. Inf. Comput. 206(7), 840\u2013868 (2008)","journal-title":"Inf. Comput."},{"doi-asserted-by":"crossref","unstructured":"Hubert, L., Barr\u00e9, N., Besson, F., Demange, D., Jensen, T., Monfort, V., Pichardie, D., Turpin, T.: Sawja: static analysis workshop for Java. In: Formal Verification of Object-Oriented Software (FoVeOOS \u201910), LNCS, vol. 6528, pp. 92\u2013106. Springer, Berlin (2010)","key":"375_CR19","DOI":"10.1007\/978-3-642-18070-5_7"},{"doi-asserted-by":"crossref","unstructured":"Huisman, M., Aktug, I., Gurov, D.: Program models for compositional verification. In: International Conference on Formal Engineering Methods (ICFEM \u201908), LNCS, vol. 5256, pp. 147\u2013166. Springer, Berlin (2008)","key":"375_CR20","DOI":"10.1007\/978-3-540-88194-0_11"},{"doi-asserted-by":"crossref","unstructured":"Huisman, M., Gurov, D.: CVPP: A tool set for compositonal verification of control-flow safety properties. In: Formal Verification of Object-Oriented Software (FoVeOOS \u201910), LNCS, vol. 6528, pp. 107\u2013121. Springer, Berlin (2010)","key":"375_CR21","DOI":"10.1007\/978-3-642-18070-5_8"},{"doi-asserted-by":"crossref","unstructured":"Jiang, S., Jiang, Y.: An analysis approach for testing exception handling programs. SIGPLAN Not. 42, 3\u20138 (2007)","key":"375_CR22","DOI":"10.1145\/1288258.1288259"},{"doi-asserted-by":"crossref","unstructured":"Jo, J.W., Chang, B.M.: Constructing control flow graph for Java by decoupling exception flow from normal flow. In: ICCSA (1), pp. 106\u2013113 (2004)","key":"375_CR23","DOI":"10.1007\/978-3-540-24707-4_14"},{"unstructured":"Kiefer, S., Schwoon, S., Suwimonteerabuth, D.: Moped\u2014a model-checker for pushdown systems (2005). http:\/\/www.informatik.uni-stuttgart.de\/fmi\/szs\/tools\/moped\/","key":"375_CR24"},{"issue":"7","key":"375_CR25","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). doi: 10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"375_CR26","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ \u03bc -calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Lindholm, T., Yellin, F., Bracha, G., Buckley, A.: The Java Virtual Machine Specification. java se 7 edition. Tech. Rep. JSR-000924, Oracle (2012)","key":"375_CR27"},{"doi-asserted-by":"publisher","unstructured":"Mihancea, P., Minea, M.: Jmodex: Model extraction for verifying security properties of web applications. In: IEEE Conference on Software Maintenance, Reengineering and Reverse Engineering (CSMR-WCRE), pp. 450\u2013453 (2014). doi: 10.1109\/CSMR-WCRE.2014.6747216","key":"375_CR28","DOI":"10.1109\/CSMR-WCRE.2014.6747216"},{"key":"375_CR29","volume-title":"Communicating and Mobile Systems: the $$\\pi $$ \u03c0","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: the $$\\pi $$ \u03c0 -Calculus, chap. 6. Cambridge University Press, New York (1999)"},{"doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE, New York (1977). doi: 10.1109\/SFCS.1977.32","key":"375_CR30","DOI":"10.1109\/SFCS.1977.32"},{"unstructured":"Schwoon, S.: Model-checking pushdown systems. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2002)","key":"375_CR31"},{"doi-asserted-by":"crossref","unstructured":"Sinha, S., Harrold, M.J.: Criteria for testing exception-handling constructs in Java programs. In: Proceedings of the IEEE International Conference on Software Maintenance, ICSM \u201999, pp. 265\u2013276. IEEE Computer Society, New York (1999)","key":"375_CR32","DOI":"10.1109\/ICSM.1999.792624"},{"key":"375_CR33","doi-asserted-by":"publisher","first-page":"849","DOI":"10.1109\/32.877846","volume":"26","author":"S Sinha","year":"2000","unstructured":"Sinha, S., Harrold, M.J.: Analysis and testing of programs with exception handling constructs. IEEE Trans. Softw. Eng. 26, 849\u2013871 (2000). doi: 10.1109\/32.877846","journal-title":"IEEE Trans. Softw. Eng."},{"doi-asserted-by":"crossref","unstructured":"Soleimanifard, S., Gurov, D.: Algorithmic verification of procedural programs in the presence of code variability. In: Post-Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS\u201914), Lecture Notes in Computer Science, vol. 8997. Springer, Berlin (2014)","key":"375_CR34","DOI":"10.1007\/978-3-319-15317-9_20"},{"unstructured":"Soleimanifard, S., Gurov, D., Huisman, M.: ProMoVer Web Interface (2012). http:\/\/www.csc.kth.se\/siavashs\/ProMoVer","key":"375_CR35"},{"doi-asserted-by":"publisher","unstructured":"Soleimanifard, S., Gurov, D., Huisman, M.: Procedure-modular specification and verification of temporal safety properties. Software & Systems Modeling, pp. 1\u201318 (2013). doi: 10.1007\/s10270-013-0321-0 . http:\/\/dx.doi.org\/","key":"375_CR36","DOI":"10.1007\/s10270-013-0321-0"},{"issue":"2","key":"375_CR37","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10270-009-0132-5","volume":"10","author":"F Spoto","year":"2011","unstructured":"Spoto, F.: Precise null-pointer analysis. Softw. Syst. Model. 10(2), 219\u2013252 (2011). doi: 10.1007\/s10270-009-0132-5","journal-title":"Softw. Syst. Model."},{"doi-asserted-by":"publisher","unstructured":"Sundaresan, V., Hendren, L., Razafimahefa, C., Vall\u00e9e-Rai, R., Lam, P., Gagnon, E., Godin, C.: Practical virtual method call resolution for java. In: Proceedings of the 15th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA \u201900, pp. 264\u2013280. ACM, New York (2000). doi: 10.1145\/353171.353189 . http:\/\/doi.acm.org\/","key":"375_CR38","DOI":"10.1145\/353171.353189"},{"unstructured":"Vall\u00e9e-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E. Co, P.: Soot\u2014A Java Optimization Framework. In: CASCON \u201999, pp. 125\u2013135 (1999). http:\/\/www.sable.mcgill.ca\/soot\/","key":"375_CR39"},{"unstructured":"Watson, T.J.: IBM: Libraries for Analysis (Wala) (2012). http:\/\/wala.sourceforge.net\/","key":"375_CR40"},{"unstructured":"Zhao, J.: Analyzing control flow in Java bytecode. In: Proceedings of the 16th Conference of Japan Society for Software Science and Technology, pp. 313\u2013316 (1999)","key":"375_CR41"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0375-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0375-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0375-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0375-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,4]],"date-time":"2022-05-04T07:31:21Z","timestamp":1651649481000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0375-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4,5]]},"references-count":41,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2016,11]]}},"alternative-id":["375"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0375-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2015,4,5]]}}}