{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:20Z","timestamp":1775868500312,"version":"3.50.1"},"reference-count":73,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,10,22]],"date-time":"2016-10-22T00:00:00Z","timestamp":1477094400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["GI 274\/6-1"],"award-info":[{"award-number":["GI 274\/6-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Research Training Group 1298 AlgoSyn"],"award-info":[{"award-number":["Research Training Group 1298 AlgoSyn"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Danish Council for Indpendent Research, Natural Sciences"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1007\/s10817-016-9389-x","type":"journal-article","created":{"date-parts":[[2016,10,22]],"date-time":"2016-10-22T02:45:54Z","timestamp":1477104354000},"page":"33-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic"],"prefix":"10.1007","volume":"58","author":[{"given":"Thomas","family":"Str\u00f6der","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Brockschmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Frohn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jera","family":"Hensel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cornelius","family":"Aschermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,22]]},"reference":[{"key":"9389_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: A framework for abstraction- and interpolation-based software verification. In: Proceedings of CAV\u201912","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"9389_CR2","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: Proceedings of FMOODS\u201908","DOI":"10.1007\/978-3-540-68863-1_2"},{"key":"9389_CR3","unstructured":"AProVE. http:\/\/aprove.informatik.rwth-aachen.de\/eval\/PointerJournal\/"},{"key":"9389_CR4","doi-asserted-by":"crossref","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Proceedings of CAV\u201906","DOI":"10.1007\/11817963_35"},{"key":"9389_CR5","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Variance analyses from invariance analyses. In: Proceedings of POPL\u201907","DOI":"10.1145\/1190216.1190249"},{"key":"9389_CR6","doi-asserted-by":"crossref","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory safety for systems-level code. In: Proceedings of CAV\u201911","DOI":"10.1007\/978-3-642-22110-1_15"},{"key":"9389_CR7","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Coq Art. Springer, 2004"},{"key":"9389_CR8","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"4","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: A Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 4, 827\u2013859 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9389_CR9","doi-asserted-by":"crossref","unstructured":"Bodin, M., Jensen, T., Schmitt, A.: Certified abstract interpretation with pretty-big-step semantics. In: Proceedings of CPP\u201915","DOI":"10.1145\/2676724.2693174"},{"issue":"2","key":"9389_CR10","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/s10703-011-0111-7","volume":"38","author":"A Bouajjani","year":"2011","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. Formal Methods Syst. Design 38(2), 158\u2013192 (2011)","journal-title":"Formal Methods Syst. Design"},{"key":"9389_CR11","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Otto, C., von Essen, C., Giesl, J.: Termination graphs for Java Bytecode. In: Verification, Induction, Termination Analysis, LNAI 6463, (2010)","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"9389_CR12","unstructured":"Brockschmidt, M., Otto, C., Giesl, J.: Modular termination proofs of recursive Java Bytecode programs by term rewriting. In: Proceedings of RTA\u201911"},{"key":"9389_CR13","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Str\u00f6der, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In: Proceedings of FoVeOOS\u201911","DOI":"10.1007\/978-3-642-31762-0_9"},{"key":"9389_CR14","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Proceedings of CAV\u201912","DOI":"10.1007\/978-3-642-31424-7_13"},{"key":"9389_CR15","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Proceedings of CAV\u201913","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"9389_CR16","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: Proceedings of SAS\u201914","DOI":"10.1007\/978-3-319-10936-7_5"},{"key":"9389_CR17","doi-asserted-by":"crossref","unstructured":"Cachera, D., Pichardie, D.: A certified denotational abstract interpreter. In: Proceedings of ITP\u201910","DOI":"10.1007\/978-3-642-14052-5_3"},{"key":"9389_CR18","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of OSDI\u201908"},{"key":"9389_CR19","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In: Proceedings of SAS\u201906","DOI":"10.1007\/11823230_13"},{"key":"9389_CR20","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Space invading systems code. In: Proceedings of LOPSTR\u201908","DOI":"10.1007\/978-3-642-00515-2_1"},{"key":"9389_CR21","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D.: Infer: An automatic program verifier for memory safety of C programs. In: Proceedings of NFM\u201911","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"9389_CR22","doi-asserted-by":"crossref","unstructured":"Chen, H.Y., David, C., Kroening, D., Schrammel, P., W\u00e4chter, N.: Synthesising interprocedural bit-precise termination proofs. In: Proceedings of ASE\u201915","DOI":"10.1109\/ASE.2015.10"},{"key":"9389_CR23","unstructured":"Clang compiler. http:\/\/clang.llvm.org"},{"issue":"5","key":"9389_CR24","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"9389_CR25","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Proceedings of RTA\u201911"},{"key":"9389_CR26","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Proceedings of SAS\u201905","DOI":"10.1007\/11547662_8"},{"key":"9389_CR27","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of PLDI\u201906","DOI":"10.1145\/1133981.1134029"},{"issue":"3","key":"9389_CR28","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/s10703-009-0087-8","volume":"35","author":"B Cook","year":"2009","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Summarization for termination: no return!. Formal Methods Syst. Design 35(3), 369\u2013387 (2009)","journal-title":"Formal Methods Syst. Design"},{"key":"9389_CR29","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL\u201978","DOI":"10.1145\/512760.512770"},{"key":"9389_CR30","doi-asserted-by":"crossref","unstructured":"David, C., Kroening, D., Lewis, M.: Unrestricted termination and non-termination arguments for bit-vector programs. In: Proceedings of ESOP\u201915","DOI":"10.1007\/978-3-662-46669-8_8"},{"key":"9389_CR31","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of TACAS\u201908","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9389_CR32","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Urban, C.: Conflict-driven conditional termination. In: Proceedings of CAV\u201915","DOI":"10.1007\/978-3-319-21668-3_16"},{"key":"9389_CR33","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: A shape analyzer based on symbolic memory graphs (competition contribution). In: Proceedings of TACAS\u201914"},{"key":"9389_CR34","unstructured":"Dutertre, B., de\u00a0Moura, L.: The Yices SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"9389_CR35","unstructured":"Falke, S., Kapur, D., Sinz. C.: Termination analysis of C programs using compiler intermediate languages. In: Proceedings of RTA\u201911"},{"key":"9389_CR36","unstructured":"Falke, S., Merz, F., Sinz, C.: LLBMC: Improved bounded model checking of C using LLVM (competition contribution). In: Proceedings of TACAS\u201913"},{"key":"9389_CR37","doi-asserted-by":"crossref","unstructured":"Fuhs, C., Giesl, J., Pl\u00fccker, M., Schneider-Kamp, P., Falke, S.: Proving termination of integer term rewriting. In: Proceedings of RTA\u201909","DOI":"10.1007\/978-3-642-02348-4_3"},{"key":"9389_CR38","doi-asserted-by":"crossref","unstructured":"Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: Proceedings of IJCAR\u201914","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"9389_CR39","doi-asserted-by":"crossref","unstructured":"Gonnord, L., Monniaux, D., Radanne, G.: Synthesis of ranking functions using extremal counterexamples. In: Proceedings of PLDI\u201915","DOI":"10.1145\/2737924.2737976"},{"key":"9389_CR40","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: An abstract domain for analyzing heap-manipulating low-level software. In: Proceedings of CAV\u201907","DOI":"10.1007\/978-3-540-73368-3_42"},{"key":"9389_CR41","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Iosif, R., Rogalewicz, A., Vojnar, T.: Proving termination of tree manipulating programs. In: Proceedings of ATVA\u201907","DOI":"10.1007\/978-3-540-75596-8_12"},{"key":"9389_CR42","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Lal, A., Nori, A., Rajamani, S.K.: Alternation for termination. In: Proceedings of SAS\u201910","DOI":"10.1007\/978-3-642-15769-1_19"},{"key":"9389_CR43","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Proceedings of ATVA\u201913","DOI":"10.1007\/978-3-319-02444-8_26"},{"key":"9389_CR44","doi-asserted-by":"crossref","unstructured":"Hensel, J., Giesl, J., Frohn, F., Str\u00f6der, T.: Proving termination of programs with bitvector arithmetic by symbolic execution. In: Proceedings of SEFM\u201916","DOI":"10.1007\/978-3-319-41591-8_16"},{"issue":"4","key":"9389_CR45","first-page":"739","volume":"32","author":"R Iosif","year":"2013","unstructured":"Iosif, R., Rogalewicz, A.: Automata-based termination proofs. Comput. Inf. 32(4), 739\u2013775 (2013)","journal-title":"Comput. Inf."},{"key":"9389_CR46","doi-asserted-by":"crossref","unstructured":"Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Proceedings of POPL\u201915","DOI":"10.1145\/2676726.2676966"},{"key":"9389_CR47","doi-asserted-by":"crossref","unstructured":"Kop, C., Nishida, N.: Automatic constrained rewriting induction towards verifying procedural programs. In: Proceedings of APLAS\u201914","DOI":"10.1007\/978-3-319-12736-1_18"},{"key":"9389_CR48","doi-asserted-by":"crossref","unstructured":"Kop, C., Nishida, N.: Constrained Term Rewriting tooL. In: Proceedings of LPAR\u201915","DOI":"10.1007\/978-3-662-48899-7_38"},{"key":"9389_CR49","doi-asserted-by":"crossref","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.\u00a0M.: Termination analysis with compositional transition invariants. In: Proceedings of CAV\u201910","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"9389_CR50","doi-asserted-by":"crossref","unstructured":"Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio A.: Proving termination of imperative programs using Max-SMT. In: Proceedings of FMCAD\u201913","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"9389_CR51","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of CGO\u201904","DOI":"10.1109\/CGO.2004.1281665"},{"key":"9389_CR52","doi-asserted-by":"crossref","unstructured":"Le, T.C., Qin, S., Chin, W.: Termination and non-termination specification inference. In: Proceedings of PLDI\u201915","DOI":"10.1145\/2737924.2737993"},{"key":"9389_CR53","unstructured":"LLVM reference manual. http:\/\/llvm.org\/docs\/LangRef.html"},{"key":"9389_CR54","unstructured":"L\u00f6we, S., Mandrykin, M., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses (competition contribution). In: Proceedings of TACAS\u201914"},{"key":"9389_CR55","unstructured":"Magill, S.: Instrumentation Analysis: An Automated Method for Producing Numeric Abstractions of Heap-Manipulating Programs. Ph.D. thesis, CMU, Pittsburgh, PA (2010). Available at http:\/\/www.cs.cmu.edu\/~smagill\/papers\/thesis.pdf"},{"key":"9389_CR56","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M., Lee, P., Tsay, Y.: Automatic numeric abstractions for heap-manipulating programs. In: Proceedings of POPL\u201910","DOI":"10.1145\/1706299.1706326"},{"issue":"1","key":"9389_CR57","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"9389_CR58","doi-asserted-by":"crossref","unstructured":"Moy, Y., March\u00e9, C.: Modular inference of subprogram contracts for safety checking. J. Symb. Comput., 45(11), 2010","DOI":"10.1016\/j.jsc.2010.06.004"},{"key":"9389_CR59","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM, 53(6), 2006","DOI":"10.1145\/1217856.1217859"},{"key":"9389_CR60","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Springer, 2002","DOI":"10.1007\/3-540-45949-9"},{"key":"9389_CR61","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of CSL\u201901","DOI":"10.1007\/3-540-44802-0_1"},{"key":"9389_CR62","unstructured":"http:\/\/fxr.watson.org\/fxr\/source\/lib\/libsa\/strlen.c?v=OPENBSD"},{"key":"9389_CR63","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proceedings of RTA\u201910"},{"key":"9389_CR64","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Proceedings of PADL\u201907","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"9389_CR65","doi-asserted-by":"crossref","unstructured":"Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of POPL\u201995","DOI":"10.1145\/199448.199462"},{"key":"9389_CR66","doi-asserted-by":"crossref","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyser for Java Bytecode based on path-length. ACM TOPLAS, 32(3), 2010","DOI":"10.1145\/1709093.1709095"},{"key":"9389_CR67","doi-asserted-by":"crossref","unstructured":"Str\u00f6der, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Proving termination and memory safety for programs with pointer arithmetic. In: Proceedings of IJCAR\u201914","DOI":"10.1007\/978-3-319-08587-6_15"},{"key":"9389_CR68","unstructured":"Str\u00f6der, T., Aschermann, C., Frohn, F., Hensel, J., Giesl, J.: AProVE: Termination and memory safety of C programs (competition contribution). In: Proceedings of TACAS\u201915"},{"key":"9389_CR69","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Proceedings of TPHOLs\u201909","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"9389_CR70","doi-asserted-by":"crossref","unstructured":"Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Proceedings of TACAS\u201911","DOI":"10.1007\/978-3-642-19835-9_9"},{"key":"9389_CR71","doi-asserted-by":"crossref","unstructured":"Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Proceedings of TACAS\u201916","DOI":"10.1007\/978-3-662-49674-9_4"},{"key":"9389_CR72","unstructured":"Wikibooks C Programming. http:\/\/en.wikibooks.org\/wiki\/C_Programming\/"},{"key":"9389_CR73","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM IR for verified program transformations. In: Proceedings of POPL\u201912"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9389-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9389-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9389-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T18:51:01Z","timestamp":1568487061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9389-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,22]]},"references-count":73,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,1]]}},"alternative-id":["9389"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9389-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,10,22]]}}}