{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T22:00:44Z","timestamp":1726005644073},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030112448"},{"type":"electronic","value":"9783030112455"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-11245-5_6","type":"book-chapter","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T18:45:18Z","timestamp":1547145918000},"page":"114-135","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Static Analysis of Binary Code with Memory Indirections Using Polyhedra"],"prefix":"10.1007","author":[{"given":"Cl\u00e9ment","family":"Ballabriga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Forget","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laure","family":"Gonnord","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Lipari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jordy","family":"Ruiz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,11]]},"reference":[{"key":"6_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"2006","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison-Wesley Longman Publishing Co. Inc., Boston (2006)","edition":"2"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Ammarguellat, Z., Harrison, III, W.L.: Automatic recognition of induction variables and recurrence relations by abstract interpretation. In: Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, PLDI 1990, pp. 283\u2013295. ACM, New York (1990)","DOI":"10.1145\/93542.93583"},{"issue":"1","key":"6_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-24723-4_2","volume-title":"Compiler Construction","author":"G Balakrishnan","year":"2004","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 5\u201323. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24723-4_2"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-16256-5_6","volume-title":"Software Technologies for Embedded and Ubiquitous Systems","author":"C Ballabriga","year":"2010","unstructured":"Ballabriga, C., Cass\u00e9, H., Rochange, C., Sainrat, P.: OTAWA: an open toolbox for adaptive WCET analysis. In: Min, S.L., Pettit, R., Puschner, P., Ungerer, T. (eds.) SEUS 2010. LNCS, vol. 6399, pp. 35\u201346. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16256-5_6"},{"issue":"2","key":"6_CR6","first-page":"39","volume":"17","author":"C Ballabriga","year":"2018","unstructured":"Ballabriga, C., Forget, J., Lipari, G.: Symbolic WCET computation. ACM Trans. Embed. Comput. Syst. (TECS) 17(2), 39 (2018)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-18275-4_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Bardin","year":"2011","unstructured":"Bardin, S., Herrmann, P., V\u00e9drine, F.: Refinement-based CFG reconstruction from unstructured programs. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 54\u201369. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_6"},{"key":"6_CR8","unstructured":"Bonenfant, A., de Michiel, M., Sainrat, P.: oRange: a tool for static loop bound analysis. In: Workshop on Resource Analysis, University of Hertfordshire, Hatfield, UK (2008)"},{"key":"6_CR9","unstructured":"Broman, D.: A brief overview of the KTA WCET tool. arXiv preprint arXiv:1712.05264 (2017)"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2012.10.003","volume":"288","author":"S Bygde","year":"2012","unstructured":"Bygde, S., Lisper, B., Holsti, N.: Fully bounded polyhedral analysis of integers with wrapping. Electron. Notes Theor. Comput. Sci. 288, 3\u201313 (2012)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-32469-7_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"L Correnson","year":"2012","unstructured":"Correnson, L., Signoles, J.: Combining analyses for C program verification. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 108\u2013130. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32469-7_8"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 84\u201396. ACM (1978). https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-662-46681-0_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Djoudi","year":"2015","unstructured":"Djoudi, A., Bardin, S.: BINSEC: binary code analysis with low-level regions. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 212\u2013217. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_17"},{"key":"6_CR14","unstructured":"Ermedahl, A., Sandberg, C., Gustafsson, J., Bygde, S., Lisper, B.: Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis. In: Rochange, C. (ed.) 7th International Workshop on Worst-Case Execution Time Analysis (WCET 2007). OpenAccess Series in Informatics (OASIcs), vol. 6. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2007)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009), pp. 127\u2013139. ACM (2009)","DOI":"10.1145\/1594834.1480898"},{"key":"6_CR16","unstructured":"Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The M\u00e4lardalen WCET benchmarks: past, present and future. In: OASIcs-OpenAccess Series in Informatics, vol. 15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2010)"},{"issue":"6","key":"6_CR17","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1145\/1273442.1250767","volume":"42","author":"B Hardekopf","year":"2007","unstructured":"Hardekopf, B., Lin, C.: The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code. ACM SIGPLAN Not. 42(6), 290\u2013299 (2007)","journal-title":"ACM SIGPLAN Not."},{"key":"6_CR18","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.entcs.2012.11.003","volume":"289","author":"J Henry","year":"2012","unstructured":"Henry, J., Monniaux, D., Moy, M.: Pagai: a path sensitive static analyser. Electron. Notes Theor. Comput. Sci. 289, 15\u201325 (2012)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2001), pp. 54\u201361. ACM, New York (2001)","DOI":"10.1145\/379605.379665"},{"issue":"2","key":"6_CR20","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Inform. 6(2), 133\u2013151 (1976)","journal-title":"Acta Inform."},{"key":"6_CR21","unstructured":"K\u00e4stner, D., et al.: Astr\u00e9e: proving the absence of runtime errors. In: Embedded Real Time Software and Systems (ERTS2 2010), p. 9, May 2010"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-662-45231-8_38","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications","author":"B Lisper","year":"2014","unstructured":"Lisper, B.: SWEET \u2013 a tool for wcet flow analysis (extended abstract). In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 482\u2013485. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-45231-8_38"},{"key":"6_CR23","unstructured":"Tamburini, P., Stagni, R., Cappello, A.: Design of a modular platform for static analysis. In: Spoto, F. (ed.) 9th Workshop on Tools for Automatic Program Analysis (TAPAS 2018). Lecture Notes in Computer Science (LNCS). Springer, Cham, p. 4, August 2018"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), pp. 54\u201363 (2006)","DOI":"10.1145\/1134650.1134659"},{"key":"6_CR25","unstructured":"Pouchet, L.N.: Polybench: the polyhedral benchmark suite (2012). http:\/\/www.cs.ucla.edu\/pouchet\/software\/polybench"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-78791-4_2","volume-title":"Compiler Construction","author":"T Reps","year":"2008","unstructured":"Reps, T., Balakrishnan, G.: Improved memory-access analysis for x86 executables. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 16\u201335. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78791-4_2"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Sepp, A., Mihaila, B., Simon, A.: Precise static analysis of binaries by extracting relational information. In: 18th Working Conference on Reverse Engineering (WCRE 2011). IEEE (2011)","DOI":"10.1109\/WCRE.2011.50"},{"key":"6_CR28","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. Technical report, New York University. Courant Institute of Mathematical Sciences. Computer Science Department (1978)"},{"issue":"2","key":"6_CR29","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"6_CR30","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-31424-7_15","volume-title":"Computer Aided Verification","author":"Arnaud J. Venet","year":"2012","unstructured":"Venet, A.: The gauge domain: scalable analysis of linear inequality invariants. In: 24th International Conference on Computer Aided Verification (CAV 2012), pp. 139\u2013154 (2012)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-11245-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,14]],"date-time":"2019-11-14T03:16:21Z","timestamp":1573701381000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-11245-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030112448","9783030112455"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11245-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cascais","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl19.sigplan.org\/track\/VMCAI-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}