{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T21:50:26Z","timestamp":1757541026560,"version":"3.37.3"},"reference-count":62,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T00:00:00Z","timestamp":1553212800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004955","name":"\u00d6sterreichische Forschungsf\u00f6rderungsgesellschaft","doi-asserted-by":"publisher","award":["850757"],"award-info":[{"award-number":["850757"]}],"id":[{"id":"10.13039\/501100004955","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Empir Software Eng"],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.1007\/s10664-019-09699-5","type":"journal-article","created":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T13:02:51Z","timestamp":1553259771000},"page":"3114-3150","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Semantics-driven extraction of timed automata from Java programs"],"prefix":"10.1007","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9337-5762","authenticated-orcid":false,"given":"Giovanni","family":"Liva","sequence":"first","affiliation":[]},{"given":"Muhammad Taimoor","family":"Khan","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Pinzger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,3,22]]},"reference":[{"key":"9699_CR1","unstructured":"Abadi M, Cardelli L (2012) A theory of objects. Springer Science & Business Media"},{"key":"9699_CR2","doi-asserted-by":"crossref","unstructured":"Abrahamson J, Beschastnikh I, Brun Y, Ernst MD (2014) Shedding light on distributed system executions. In: Companion proceedings of the 36th international conference on software engineering. ACM, pp 598\u2013599","DOI":"10.1145\/2591062.2591134"},{"key":"9699_CR3","doi-asserted-by":"crossref","unstructured":"Alur R (1999) Timed automata. In: International conference on computer aided verification (CAV). Springer, pp 8\u201322","DOI":"10.1007\/3-540-48683-6_3"},{"issue":"2","key":"9699_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126 (2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"9699_CR5","unstructured":"Baier C, Katoen JP, Larsen KG (2008) Principles of model checking. MIT Press"},{"issue":"5","key":"9699_CR6","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1109\/TDSC.2010.38","volume":"8","author":"A Baliga","year":"2011","unstructured":"Baliga A, Ganapathy V, Iftode L (2011) Detecting kernel-level rootkits using data structure invariants. IEEE Trans Depend Sec Comput 8(5):670\u2013684","journal-title":"IEEE Trans Depend Sec Comput"},{"key":"9699_CR7","unstructured":"Barrett C, Stump A, Tinelli C, et al. (2010) The SMT-LIB standard: version 2.0. In: Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England), vol 13, p 14"},{"key":"9699_CR8","doi-asserted-by":"crossref","unstructured":"Behrmann G, David A, Larsen KG (2004) A tutorial on UPPAAL. In: Formal methods for the design of real-time systems. Springer, pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"9699_CR9","doi-asserted-by":"crossref","unstructured":"Bengtsson J, Griffioen WD, Kristoffersen KJ, Larsen KG, Larsson F, Pettersson P, Yi W (1996) Verification of an audio protocol with bus collision using UPPAAL. 1102. Springer, pp 244\u2013256. http:\/\/www.docs.uu.se\/docs\/rtmv\/papers\/bgkllpw:cav96.ps.gz","DOI":"10.1007\/3-540-61474-5_73"},{"key":"9699_CR10","doi-asserted-by":"crossref","unstructured":"Beschastnikh I, Brun Y, Schneider S, Sloan M, Ernst MD (2011) Leveraging existing instrumentation to automatically infer invariant-constrained models. In: Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on foundations of software engineering. ACM, pp 267\u2013277","DOI":"10.1145\/2025113.2025151"},{"issue":"3","key":"9699_CR11","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/2094091.2094101","volume":"45","author":"I Beschastnikh","year":"2012","unstructured":"Beschastnikh I, Brun Y, Ernst MD, Krishnamurthy A, Anderson TE (2012) Mining temporal invariants from partially ordered logs. ACM SIGOPS Oper Syst Rev 45(3):39\u201346","journal-title":"ACM SIGOPS Oper Syst Rev"},{"key":"9699_CR12","doi-asserted-by":"crossref","unstructured":"Beschastnikh I, Brun Y, Ernst MD, Krishnamurthy A (2014) Inferring models of concurrent systems from logs of their behavior with CSight. In: Proceedings of the 36th international conference on software engineering. ACM, pp 468\u2013479","DOI":"10.1145\/2568225.2568246"},{"issue":"2","key":"9699_CR13","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1145\/2927299.2940294","volume":"14","author":"I Beschastnikh","year":"2016","unstructured":"Beschastnikh I, Wang P, Brun Y, Ernst MD (2016) Debugging distributed systems. Queue 14(2):50","journal-title":"Queue"},{"key":"9699_CR14","doi-asserted-by":"crossref","unstructured":"Bogdanas D, Ro\u015fu G (2015) K-Java: a complete semantics of Java. In: Proceedings of the ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL). ACM, pp 445\u2013456","DOI":"10.1145\/2676726.2676982"},{"issue":"6","key":"9699_CR15","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1109\/2.846318","volume":"33","author":"G Bollella","year":"2000","unstructured":"Bollella G, Gosling J (2000) The real-time specification for Java. Computer 33(6):47\u201354","journal-title":"Computer"},{"issue":"2-3","key":"9699_CR16","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.tcs.2004.11.008","volume":"336","author":"E B\u00f6rger","year":"2005","unstructured":"B\u00f6rger E, Fruja NG, Gervasi V, St\u00e4rk RF (2005) A high-level modular definition of the semantics of C#. Theor Comput Sci 336(2-3):235\u2013284","journal-title":"Theor Comput Sci"},{"key":"9699_CR17","doi-asserted-by":"crossref","unstructured":"Cardelli L, Gordon AD (1998) Mobile ambients. In: International conference on foundations of software science and computation structure. Springer, pp 140\u2013155","DOI":"10.1007\/BFb0053547"},{"key":"9699_CR18","unstructured":"Cicirelli F, Furfaro A, Nigro L, Pupo F (2013) Modelling Java concurrency: an approach and a UPPAAL library. In: Federated conference on computer science and information systems (FedCSIS). IEEE, pp 1373\u20131380"},{"key":"9699_CR19","unstructured":"Deharbe D, Fontaine P, Paleo BW (2011) Quantifier inference rules for SMT proofs. In: First international workshop on proof eXchange for theorem proving (PxTP)"},{"issue":"10","key":"9699_CR20","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1145\/355604.361591","volume":"15","author":"EW Dijkstra","year":"1972","unstructured":"Dijkstra EW (1972) The humble programmer. Commun ACM 15(10):859\u2013866","journal-title":"Commun ACM"},{"issue":"1-3","key":"9699_CR21","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C (2007) The Daikon system for dynamic detection of likely invariants. Sci Comput Program 69(1-3):35\u201345","journal-title":"Sci Comput Program"},{"key":"9699_CR22","doi-asserted-by":"crossref","unstructured":"Farzan A, Chen F, Meseguer J, Ros\u0307u G (2004) Formal analysis of Java programs in JavaFAN. In: International conference on computer aided verification. Springer, pp 501\u2013505","DOI":"10.1007\/978-3-540-27813-9_46"},{"key":"9699_CR23","doi-asserted-by":"crossref","unstructured":"Filaretti D, Maffeis S (2014) An executable formal semantics of PHP. In: European conference on object-oriented programming. Springer, pp 567\u2013592","DOI":"10.1007\/978-3-662-44202-9_23"},{"key":"9699_CR24","doi-asserted-by":"crossref","unstructured":"Flatt M, Krishnamurthi S, Felleisen M (1998) Classes and mixins. In: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, pp 171\u2013183","DOI":"10.1145\/268946.268961"},{"key":"9699_CR25","doi-asserted-by":"crossref","unstructured":"Georgiou C, Musial PM, Ploutarchou C (2013) Tempo-toolkit: tempo to Java translation module. In: International symposium on network computing and applications (NCA). IEEE, pp 235\u2013242","DOI":"10.1109\/NCA.2013.17"},{"key":"9699_CR26","first-page":"3","volume":"3","author":"D Guth","year":"2013","unstructured":"Guth D (2013) . A formal semantics of Python 3:3","journal-title":"A formal semantics of Python"},{"key":"9699_CR27","doi-asserted-by":"crossref","unstructured":"Hakimipour N, Strooper P, Wellings A (2010) TART: timed-automata to real-time Java tool. In: International conference on software engineering and formal methods (SEFM). IEEE, pp 299\u2013309","DOI":"10.1109\/SEFM.2010.39"},{"key":"9699_CR28","doi-asserted-by":"crossref","unstructured":"Hatcliff J, Dwyer M (2001) Using the Bandera tool set to model-check properties of concurrent Java software. In: International conference on concurrency theory (CONCUR). Springer, pp 39\u201358","DOI":"10.1007\/3-540-44685-0_5"},{"key":"9699_CR29","doi-asserted-by":"crossref","unstructured":"Hathhorn C, Ellison C, Ros\u0307u G. (2015) Defining the undefinedness of C. In: ACM SIGPLAN notices, vol 50. ACM, pp 336\u2013345","DOI":"10.1145\/2813885.2737979"},{"issue":"4","key":"9699_CR30","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund K, Pressburger T (2000) Model checking Java programs using Java pathfinder. Int J Softw Tools Technol Transfer (STTT) 2(4):366\u2013381","journal-title":"Int J Softw Tools Technol Transfer (STTT)"},{"key":"9699_CR31","unstructured":"Hennessy M (1988) Algebraic theory of processes. MIT press"},{"key":"9699_CR32","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Necula GC, Jhala R, Sutre G, Majumdar R, Weimer W (2002) Temporal-safety proofs for systems code. In: International conference on computer aided verification (CAV). Springer, pp 526\u2013538","DOI":"10.1007\/3-540-45657-0_45"},{"key":"9699_CR33","unstructured":"Hopkins WG (2014) A new view of statistics. Internet Society for Sport Science"},{"issue":"1","key":"9699_CR34","first-page":"43","volume":"8","author":"T Hune","year":"2001","unstructured":"Hune T, Larsen KG, Pettersson P (2001) Guided synthesis of control programs using UPPAAL. Nord J Comput 8(1):43\u201364","journal-title":"Nord J Comput"},{"key":"9699_CR35","doi-asserted-by":"crossref","unstructured":"Jayaraman S, Hari D, Jayaraman B (2015) Consistency of Java run-time behavior with design-time specifications. In: International conference on contemporary computing (IC3). IEEE, pp 548\u2013554","DOI":"10.1109\/IC3.2015.7346742"},{"issue":"1","key":"9699_CR36","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1109\/JPROC.2017.2725642","volume":"106","author":"MT Khan","year":"2018","unstructured":"Khan MT, Serpanos D, Shrobe H (2018) ARMET: behavior-based secure and resilient industrial control systems. Proc IEEE 106(1):129\u2013143","journal-title":"Proc IEEE"},{"issue":"3","key":"9699_CR37","first-page":"14","volume":"14","author":"CY Laporte","year":"2012","unstructured":"Laporte CY, Nabil B, Mikel D (2012) Measuring the cost of software quality of a large software project at bombardier transportation: a case study. Softw Qual Manage 14(3):14\u201331","journal-title":"Softw Qual Manage"},{"key":"9699_CR38","unstructured":"Larsen KG, Pettersson P, Yi W (1995) Diagnostic model-checking for real-time systems. In: Proc. of workshop on verification and control of hybrid systems III, 1066. Springer, pp 575\u2013586"},{"issue":"1-2","key":"9699_CR39","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transfer (STTT) 1(1-2):134\u2013152","journal-title":"Int J Softw Tools Technol Transfer (STTT)"},{"key":"9699_CR40","unstructured":"Le TDB, Le XBD, Lo D, Beschastnikh I (2015) Synergizing specification miners through model fissions and fusions (t). In: 2015 30th IEEE\/ACM International conference on automated software engineering (ASE). IEEE, pp 115\u2013125"},{"key":"9699_CR41","doi-asserted-by":"crossref","unstructured":"Lemieux C, Park D, Beschastnikh I (2015) General LTL specification mining (t). In: 2015 30th IEEE\/ACM International conference on automated software engineering (ASE). IEEE, pp 81\u201392","DOI":"10.1109\/ASE.2015.71"},{"key":"9699_CR42","unstructured":"Lindahl M, Pettersson P, Yi W (1998) Formal design and analysis of a gear-box controller. In: Proc.of the 4th workshop on tools and algorithms for the construction and analysis of systems, no. 1384 in lecture notes in computer science. Springer, pp 281\u2013297"},{"key":"9699_CR43","doi-asserted-by":"crossref","unstructured":"Liva G, Khan MT, Pinzger M (2017) Extracting timed automata from Java methods. In: Proceedings of the IEEE 17th international working conference on source code analysis and manipulation (SCAM), pp 91\u2013100","DOI":"10.1109\/SCAM.2017.9"},{"key":"9699_CR44","doi-asserted-by":"crossref","unstructured":"Liva G, Khan MT, Spegni F, Spalazzi L, Bollin A, Pinzger M (2018) Modeling time in Java programs for automatic error detection. In: Proceedings of the IEEE\/ACM conference on formal methods in software engineering (FormaliSE 2018). IEEE Press","DOI":"10.1145\/3193992.3193997"},{"key":"9699_CR45","doi-asserted-by":"crossref","unstructured":"Lo D, Mariani L, Pezz\u00e8 M (2009) Automatic steering of behavioral model inference. In: Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering (ESEC\/FSE). ACM, pp 345\u2013354","DOI":"10.1145\/1595696.1595761"},{"key":"9699_CR46","doi-asserted-by":"crossref","unstructured":"McCarthy J (1964) A formal description of a subset of ALGOL. Tech. rep., Stanford University Department of Computer Science","DOI":"10.21236\/AD0785050"},{"key":"9699_CR47","doi-asserted-by":"crossref","unstructured":"McCarthy J (1993) Towards a mathematical science of computation. In: Program verification. Springer, pp 35\u201356","DOI":"10.1007\/978-94-011-1793-7_2"},{"key":"9699_CR48","unstructured":"Milner R (1999) Communication and mobile systems: the \u03c0-calculus. Cambridge Uni"},{"key":"9699_CR49","doi-asserted-by":"crossref","unstructured":"Pacheco C, Ernst MD (2005) Eclat: automatic generation and classification of test inputs. In: 19th European conference on ECOOP 2005 \u2014 object-oriented programming. Glasgow, pp 504\u2013527","DOI":"10.1007\/11531142_22"},{"key":"9699_CR50","doi-asserted-by":"crossref","unstructured":"Park D, \u015etef\u0103nescu A, Ro\u015fu G (2015) KJS: a complete formal semantics of Javascript. In: Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation (PLDI\u201915). ACM, pp 346\u2013356","DOI":"10.1145\/2737924.2737991"},{"issue":"3","key":"9699_CR51","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"GD Plotkin","year":"1977","unstructured":"Plotkin GD (1977) LCF considered as a programming language. Theor Comput Sci 5(3):223\u2013255","journal-title":"Theor Comput Sci"},{"key":"9699_CR52","unstructured":"Plotkin GD (1981) A structural approach to operational semantics. Computer Science Department Aarhus University Denmark"},{"issue":"6","key":"9699_CR53","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu G., Serba\u0307nuta\u0307 TF (2010) An overview of the K semantic framework. J Logic Algebraic Program 79(6):397\u2013434","journal-title":"J Logic Algebraic Program"},{"key":"9699_CR54","unstructured":"Sangiorgi D, Walker D (2003) The pi-calculus: a theory of mobile processes. Cambridge University Press"},{"issue":"10","key":"9699_CR55","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/2398857.2384624","volume":"47","author":"TW Schiller","year":"2012","unstructured":"Schiller TW, Ernst MD (2012) Reducing the barriers to writing verified specifications. ACM SIGPLAN Not 47(10):95\u2013112","journal-title":"ACM SIGPLAN Not"},{"key":"9699_CR56","unstructured":"St\u00e4rk RF, Schmid J, B\u00f6rger E (2012) Java and the Java virtual machine: definition, verification, validation. Springer Science & Business Media"},{"key":"9699_CR57","unstructured":"Steel T (1969) A formalization of semantics for programming language description. In: Proc. IFIP WG formal language description languages for computer programming, pp 25\u201336"},{"key":"9699_CR58","doi-asserted-by":"crossref","unstructured":"Tristan JB (2009) Formal verification of translation validators. Ph.D. thesis Universit\u00e9 Paris 7 Diderot","DOI":"10.1145\/1328438.1328444"},{"key":"9699_CR59","doi-asserted-by":"crossref","unstructured":"Walkinshaw N, Bogdanov K (2008) Inferring finite-state models with temporal constraints. In: Proceedings of the IEEE\/ACM international conference on automated software engineering (ASE). IEEE Computer Society, pp 248\u2013257","DOI":"10.1109\/ASE.2008.35"},{"issue":"1","key":"9699_CR60","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright AK, Felleisen M (1994) A syntactic approach to type soundness. Inf Comput 115(1):38\u201394","journal-title":"Inf Comput"},{"key":"9699_CR61","doi-asserted-by":"crossref","unstructured":"Yang Y, Jiang Y, Gu M, Sun J (2016) Verifying Simulink Stateflow model: timed automata approach. In: Proceedings of the IEEE\/ACM international conference on automated software engineering (ASE). ACM, pp 852\u2013857","DOI":"10.1145\/2970276.2970293"},{"issue":"1-2","key":"9699_CR62","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine S (1997) Kronos: a verification tool for real-time systems. Int J Softw Tools Technol Transfer 1(1-2):123\u2013133","journal-title":"Int J Softw Tools Technol Transfer"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-019-09699-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10664-019-09699-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-019-09699-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,14]],"date-time":"2022-09-14T06:06:22Z","timestamp":1663135582000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10664-019-09699-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3,22]]},"references-count":62,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2019,10]]}},"alternative-id":["9699"],"URL":"https:\/\/doi.org\/10.1007\/s10664-019-09699-5","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"type":"print","value":"1382-3256"},{"type":"electronic","value":"1573-7616"}],"subject":[],"published":{"date-parts":[[2019,3,22]]},"assertion":[{"value":"22 March 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}