{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T14:50:02Z","timestamp":1768315802580,"version":"3.49.0"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2017,12,10]],"date-time":"2017-12-10T00:00:00Z","timestamp":1512864000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/H017585\/1"],"award-info":[{"award-number":["EP\/H017585\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"H2020 FET OPEN","award":["712689 SC"],"award-info":[{"award-number":["712689 SC"]}]},{"name":"ERC project","award":["280053 \u201cCPROVER.\u201d"],"award-info":[{"award-number":["280053 \u201cCPROVER.\u201d"]}]},{"name":"VeTeSS: Verification and Testing to Support Functional Safety Standards, Artemis Joint Undertaking","award":["295311"],"award-info":[{"award-number":["295311"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2018,3,31]]},"abstract":"<jats:p>Non-termination is the root cause of a variety of program bugs, such as hanging programs and denial-of-service vulnerabilities. This makes an automated analysis that can prove the absence of such bugs highly desirable. To scale termination checks to large systems, an interprocedural termination analysis seems essential. This is a largely unexplored area of research in termination analysis, where most effort has focussed on small but difficult single-procedure problems.<\/jats:p>\n          <jats:p>We present a modular termination analysis for C programs using template-based interprocedural summarisation. Our analysis combines a context-sensitive, over-approximating forward analysis with the inference of under-approximating preconditions for termination. Bit-precise termination arguments are synthesised over lexicographic linear ranking function templates. Our experimental results show the advantage of interprocedural reasoning over monolithic analysis in terms of efficiency, while retaining comparable precision.<\/jats:p>","DOI":"10.1145\/3121136","type":"journal-article","created":{"date-parts":[[2017,12,11]],"date-time":"2017-12-11T13:26:47Z","timestamp":1512998807000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Bit-Precise Procedure-Modular Termination Analysis"],"prefix":"10.1145","volume":"40","author":[{"given":"Hong-Yi","family":"Chen","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, United Kingdom"}]},{"given":"Cristina","family":"David","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6681-5283","authenticated-orcid":false,"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, United Kingdom"}]},{"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[{"name":"School of Engineering and Informatics, University of Sussex, United Kingdom"}]},{"given":"Bj\u00f6rn","family":"Wachter","sequence":"additional","affiliation":[{"name":"SSW-Trading GmbH, Oststeinbek, Germany"}]}],"member":"320","published-online":{"date-parts":[[2017,12,10]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2LS. 2016. 2LS: Static Analyzer and Verifier. Retrieved from http:\/\/www.cprover.org\/2LS (version 0.4)."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.04.006"},{"key":"e_1_2_1_3_1","volume-title":"COSTA: Design and implementation of a cost and termination analyzer for java bytecode. In Formal Methods for Components and Objects (LNCS)","author":"Albert Elvira","year":"2007","unstructured":"Elvira Albert, Puri Arenas, Samir Genaim, German Puebla, and Damiano Zanardini. 2007. COSTA: Design and implementation of a cost and termination analyzer for java bytecode. In Formal Methods for Components and Objects (LNCS), Vol. 5382. Springer, 113--132."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9400-6"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882102"},{"key":"e_1_2_1_7_1","unstructured":"Apache CVE-2009-1890. 2009. Apache Common Vulnerabilities and Exposures CVE-2009-1890. Retrieved from http:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi&quest;name&equals;CVE-2009-1890."},{"key":"e_1_2_1_8_1","volume-title":"Automated Program Verification Environment (AProVE).","author":"VE.","year":"2016","unstructured":"AProVE. 2016. Automated Program Verification Environment (AProVE). Retrieved from https:\/\/sv-comp.sosy-lab.org\/2016\/downloads\/AProVE2016.zip (SV-COMP 2016)."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429078"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629488"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_35"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_18"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_9"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2866575"},{"key":"e_1_2_1_18_1","volume-title":"Automated Software Engineering","author":"Chen Hong-Yi","unstructured":"Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, and Bj\u00f6rn Wachter. 2015. Synthesising interprocedural bit-precise termination proofs. In Automated Software Engineering. IEEE Computer Society, 53--64."},{"key":"e_1_2_1_19_1","volume-title":"O\u2019Hearn","author":"Chen Hong Yi","year":"2014","unstructured":"Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O\u2019Hearn. 2014. Proving nontermination via safety. In Tools and Algorithms for the Construction and Analysis of Systems (LNCS), Vol. 8413. Springer, 156--171."},{"key":"e_1_2_1_20_1","volume-title":"Automated Technology for Verification and Analysis (LNCS)","author":"Chen Hong Yi","unstructured":"Hong Yi Chen, Supratik Mukhopadhyay, and Zheng Lu. 2013. Control flow refinement and symbolic computation of average case bound. In Automated Technology for Verification and Analysis (LNCS), Vol. 8172. Springer, 334--348."},{"key":"e_1_2_1_21_1","volume-title":"CLAPACK Linear Algebra Library.","author":"CLAPACK","year":"2014","unstructured":"CLAPACK 2014. (2014). CLAPACK Linear Algebra Library. Retrieved from http:\/\/www.netlib.org\/clapack\/cblas\/sasum.c."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_32"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_19"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Byron Cook Andreas Podelski and Andrey Rybalchenko. 2006. Termination proofs for systems code. In Programming Language Design and Implementation. ACM 415--426. 10.1145\/1133981.1134029","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Byron Cook Andreas Podelski and Andrey Rybalchenko. 2007. Proving thread termination. In Programming Language Design and Implementation. ACM 320--330. 10.1145\/1250734.1250771","DOI":"10.1145\/1250734.1250771"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Principles of Programming Languages. 238--252. 10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_29_1","unstructured":"CppInv. 2015. CppInv Termination Prover. Retrieved from http:\/\/www.lsi.upc.edu\/ albert\/cppinv-term-bin.tar.gz."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_8"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/647170.718291"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_21"},{"key":"e_1_2_1_33_1","volume-title":"Programming Languages and Systems -- 12th Asian Symposium. 275--295.","author":"Flores-Montoya Antonio","unstructured":"Antonio Flores-Montoya and Reiner H\u00e4hnle. 2014. Resource analysis of complex programs with cost equations. In Programming Languages and Systems -- 12th Asian Symposium. 275--295."},{"key":"e_1_2_1_34_1","unstructured":"FuncTion. 2015. FuncTion Termination Prover. Retrieved from http:\/\/www.di.ens.fr\/ urban\/sv-comp2015.zip (version SV-COMP-2015)."},{"key":"e_1_2_1_35_1","volume-title":"Computer-Aided Verification (LNCS)","author":"Ganty Pierre","unstructured":"Pierre Ganty and Samir Genaim. 2013. Proving termination starting from the end. In Computer-Aided Verification (LNCS), Vol. 8044. Springer, 397--412."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392389.2392396"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002236"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Laure Gonnord David Monniaux and Gabriel Radanne. 2015. Synthesis of ranking functions using extremal counterexamples. In Programming Language Design and Implementation. ACM 608--618. 10.1145\/2737924.2737976","DOI":"10.1145\/2737924.2737976"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Sergey Grebenshchikov Nuno P. Lopes Corneliu Popeea and Andrey Rybalchenko. 2012. Synthesizing software verifiers from proof rules. In Programming Language Design and Implementation. 405--416. 10.1145\/2254064.2254112","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","unstructured":"Sumit Gulwani Sagar Jain and Eric Koskinen. 2009. Control-flow refinement and progress invariants for bound analysis. In Programming Language Design and Implementation. ACM 375--385. 10.1145\/1542476.1542518","DOI":"10.1145\/1542476.1542518"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Sumit Gulwani Saurabh Srivastava and Ramarathnam Venkatesan. 2008. Program analysis as constraint solving. In Programming Language Design and Implementation. ACM 281--292. 10.1145\/1375581.1375616","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Ashutosh Gupta Thomas A. Henzinger Rupak Majumdar Andrey Rybalchenko and Ru-Gang Xu. 2008. Proving non-termination. In Principles of Programming Languages. ACM 147--158. 10.1145\/1328438.1328459","DOI":"10.1145\/1328438.1328459"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Ashutosh Gupta Corneliu Popeea and Andrey Rybalchenko. 2011. Predicate abstraction and refinement for verifying multi-threaded programs. In Principles of Programming Languages. ACM 331--344. 10.1145\/1926385.1926424","DOI":"10.1145\/1926385.1926424"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882113"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_68"},{"key":"e_1_2_1_48_1","volume-title":"Automated Technology for Verification and Analysis","author":"Heizmann Matthias","unstructured":"Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski. 2013. Linear ranking for linear lasso programs. In Automated Technology for Verification and Analysis. Springer, 365--380."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_53"},{"key":"e_1_2_1_50_1","volume-title":"Software Engineering and Formal Methods (LNCS)","author":"Hensel Jera","unstructured":"Jera Hensel, J\u00fcrgen Giesl, Florian Frohn, and Thomas Str\u00f6der. 2016. Proving termination of programs with bitvector arithmetic by symbolic execution. In Software Engineering and Formal Methods (LNCS), Vol. 9763. Springer, 234--252."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068402001436"},{"key":"e_1_2_1_53_1","unstructured":"KiTTeL\/KoAT. 2016. KITTeL\/KoAT Termination Prover. Retrieved from https:\/\/github.com\/s-falke\/kittel-koat (version 6ee36da)."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29709-0_20"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","unstructured":"Jens Knoop Laura Kov\u00e1cs and Jakob Zwirchmayr. 2012. r-TuBound: Loop bounds for WCET analysis (tool paper). In Logic for Programming Artificial Intelligence and Reasoning LPAR. 435--444. 10.1007\/978-3-642-28717-6_34","DOI":"10.1007\/978-3-642-28717-6_34"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_54"},{"key":"e_1_2_1_58_1","volume-title":"Formal Methods and Software Engineering (LNCS)","author":"Le Ton Chanh","unstructured":"Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, and Wei-Ngan Chin. 2014. A resource-based logic for termination and non-termination proofs. In Formal Methods and Software Engineering (LNCS), Vol. 8829. Springer, 267--283."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","unstructured":"Ton Chanh Le Shengchao Qin and Wei-Ngan Chin. 2015. Termination and non-termination specification inference. In Programming Language Design and Implementation. ACM 489--498. 10.1145\/2737924.2737993","DOI":"10.1145\/2737924.2737993"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_12"},{"key":"e_1_2_1_61_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (LNCS)","author":"Leike Jan","unstructured":"Jan Leike and Matthias Heizmann. 2014. Ranking templates for linear loops. In Tools and Algorithms for the Construction and Analysis of Systems (LNCS), Vol. 8413. Springer, 172--186."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","unstructured":"Yi Li Aws Albarghouthi Zachary Kincaid Arie Gurfinkel and Marsha Chechik. 2014. Symbolic optimization with SMT solvers. In Principles of Programming Languages. ACM 607--618. 10.1145\/2535838.2535857","DOI":"10.1145\/2535838.2535857"},{"key":"e_1_2_1_63_1","unstructured":"llvm2KITTeL. 2016. llvm2KITTeL Converter. Retrieved from https:\/\/github.com\/hkhlaaf\/llvm2kittel (version e37be65e)."},{"key":"e_1_2_1_64_1","unstructured":"Loopus. 2014. Loopus Termination Prover. Retrieved from http:\/\/forsyte.at\/software\/loopus\/ with http:\/\/sourceforge.net\/projects\/virtualboximage\/files\/Ubuntu&percent;20Linux\/11.10\/ubuntu_11.10-x86.7z\/download."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","unstructured":"Stephen Magill Ming-Hsien Tsai Peter Lee and Yih-Kuen Tsay. 2010. Automatic numeric abstractions for heap-manipulating programs. In Principles of Programming Languages. ACM 211--222. 10.1145\/1706299.1706326","DOI":"10.1145\/1706299.1706326"},{"key":"e_1_2_1_66_1","volume-title":"Computer-Aided Verification (LNCS)","author":"Manevich Roman","unstructured":"Roman Manevich, Boris Dogadov, and Noam Rinetzky. 2016. From shape analysis to termination analysis in linear time. In Computer-Aided Verification (LNCS), Vol. 9779. Springer, 426--446."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.09.008"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_25"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2851613.2851834"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792775"},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming. 7--21","author":"Mesnard Fr\u00e9d\u00e9ric","year":"1996","unstructured":"Fr\u00e9d\u00e9ric Mesnard. 1996. Inferring left-terminating classes of queries for constraint logic programs. In Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming. 7--21."},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42347"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_8"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_17"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787526.1787548"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","unstructured":"Mads Rosendahl. 1989. Automatic complexity analysis. In Functional Programming Languages and Computer Architecture. ACM 144--156. 10.1145\/99370.99381","DOI":"10.1145\/99370.99381"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190083"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"e_1_2_1_82_1","volume-title":"HCVS@ETAPS 2016 (EPTCS)","author":"Schrammel Peter","unstructured":"Peter Schrammel. 2016. Challenges in decomposing encodings of verification problems. In HCVS@ETAPS 2016 (EPTCS), Vol. 219. 29--32."},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_56"},{"key":"e_1_2_1_84_1","unstructured":"SeaHorn. 2016. SeaHorn A Verification Framework. Retrieved from https:\/\/sv-comp.sosy-lab.org\/2016\/downloads\/SeaHorn-0.1.0-Linux-x86_64.tar.gz."},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709095"},{"key":"e_1_2_1_87_1","unstructured":"SV-COMP. 2016. Competition on Software Verification (SV-COMP). Retrieved from https:\/\/github.com\/sosy-lab\/sv-benchmarks\/releases\/tag\/svcomp16."},{"key":"e_1_2_1_88_1","unstructured":"T2. 2016. T2 Temporal Logic Prover. Retrieved from https:\/\/github.com\/mmjb\/T2 (version 90c5d0e)."},{"key":"e_1_2_1_89_1","unstructured":"TAN. 2014. TAN Termination Prover. Retrieved from http:\/\/www.cprover.org\/termination\/ (version SV-COMP-2014)."},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"e_1_2_1_91_1","volume-title":"Systems 8 Structures 47","author":"Urban Caterina","year":"2017","unstructured":"Caterina Urban and Antoine Min\u00e9. 2017. Inference of ranking functions for proving temporal properties by abstract interpretation. Computer Languages, Systems 8 Structures 47 (2017), 77--103."},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/361002.361016"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3121136","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3121136","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:39:24Z","timestamp":1750217964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3121136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,10]]},"references-count":93,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,3,31]]}},"alternative-id":["10.1145\/3121136"],"URL":"https:\/\/doi.org\/10.1145\/3121136","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,10]]},"assertion":[{"value":"2015-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}