{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T21:14:56Z","timestamp":1764364496603,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030582975"},{"type":"electronic","value":"9783030582982"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-58298-2_3","type":"book-chapter","created":{"date-parts":[[2020,8,28]],"date-time":"2020-08-28T18:04:52Z","timestamp":1598637892000},"page":"93-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Skylines for Symbolic Energy Consumption Analysis"],"prefix":"10.1007","author":[{"given":"Markus","family":"Klinik","sequence":"first","affiliation":[]},{"given":"Bernard van","family":"Gastel","sequence":"additional","affiliation":[]},{"given":"Cynthia","family":"Kop","sequence":"additional","affiliation":[]},{"given":"Marko van","family":"Eekelen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,8,29]]},"reference":[{"unstructured":"Arduino project hub. https:\/\/create.arduino.cc\/projecthub. Accessed 01 May 2020","key":"3_CR1"},{"unstructured":"SECA project wiki. https:\/\/gitlab.science.ru.nl\/mklinik\/eca-symbolic-execution\/-\/wikis\/home. Accessed 06 Feb 2020","key":"3_CR2"},{"unstructured":"SECA source code repository. https:\/\/gitlab.science.ru.nl\/mklinik\/eca-symbolic-execution. Accessed 29 Jan 2020","key":"3_CR3"},{"issue":"5","key":"3_CR4","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/1735223.1735245","volume":"53","author":"S Albers","year":"2010","unstructured":"Albers, S.: Energy-efficient algorithms. Commun. ACM 53(5), 86\u201396 (2010)","journal-title":"Commun. ACM"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-92188-2_5","volume-title":"Formal Methods for Components and Objects","author":"E Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: Design and implementation of a cost and termination analyzer for Java bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 113\u2013132. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-92188-2_5"},{"issue":"3","key":"3_CR6","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/j.tcs.2007.09.003","volume":"389","author":"D Aspinall","year":"2007","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.W., Momigliano, A.: A program logic for resources. Theor. Comput. Sci. 389(3), 411\u2013445 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2007.09.003","journal-title":"Theor. Comput. Sci."},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-11957-6_6","volume-title":"Programming Languages and Systems","author":"R Atkey","year":"2010","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 85\u2013103. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_6"},{"issue":"2","key":"3_CR8","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/342001.339657","volume":"28","author":"D Brooks","year":"2000","unstructured":"Brooks, D., Tiwari, V., Martonosi, M.: Wattch: a framework for architectural-level power analysis and optimizations. SIGARCH Comput. Arch. News 28(2), 83\u201394 (2000)","journal-title":"SIGARCH Comput. Arch. News"},{"issue":"10","key":"3_CR9","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1145\/2398857.2384676","volume":"47","author":"M Cohen","year":"2012","unstructured":"Cohen, M., Zhu, H.S., Senem, E.E., Liu, Y.D.: Energy types. SIGPLAN Not. 47(10), 831\u2013850 (2012)","journal-title":"SIGPLAN Not."},{"unstructured":"van Gastel, B.: Assessing sustainability of software - analysing correctness, memory and energy consumption. Ph.D. thesis, Open University (2016)","key":"3_CR10"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-46559-3_2","volume-title":"Foundational and Practical Aspects of Resource Analysis","author":"B van Gastel","year":"2016","unstructured":"van Gastel, B., Kersten, R., van Eekelen, M.: Using dependent types to define energy augmented semantics of programs. In: van Eekelen, M., Dal Lago, U. (eds.) FOPARA 2015. LNCS, vol. 9964, pp. 20\u201339. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46559-3_2"},{"doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Ball, T., Sagiv, M. (eds.) POPL 2011, pp. 357\u2013370. ACM (2011)","key":"3_CR12","DOI":"10.1145\/1925844.1926427"},{"doi-asserted-by":"publisher","unstructured":"Jayaseelan, R., Mitra, T., Li, X.: Estimating the worst-case energy consumption of embedded software. In: Proceedings of RTAS 2006, pp. 81\u201390. IEEE (2006). https:\/\/doi.org\/10.1109\/RTAS.2006.17","key":"3_CR13","DOI":"10.1109\/RTAS.2006.17"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/11767589_15","volume-title":"Petri Nets and Other Models of Concurrency - ICATPN 2006","author":"MNO Junior","year":"2006","unstructured":"Junior, M.N.O., et al.: Analyzing software performance and energy consumption of embedded systems by probabilistic modeling: an approach based on coloured petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 261\u2013281. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11767589_15"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-319-14125-1_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"U Liqat","year":"2014","unstructured":"Liqat, U., Kerrison, S., Serrano, A., Georgiou, K., Lopez-Garcia, P., Grech, N., Hermenegildo, M.V., Eder, K.: Energy consumption analysis of programs based on XMOS ISA-level models. In: Gupta, G., Pe\u00f1a, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 72\u201390. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-14125-1_5"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-12466-7_6","volume-title":"Foundational and Practical Aspects of Resource Analysis","author":"R Kersten","year":"2014","unstructured":"Kersten, R., Toldin, P.P., van Gastel, B., van Eekelen, M.: A hoare logic for energy consumption analysis. In: Dal Lago, U., Pe\u00f1a, R. (eds.) FOPARA 2013. LNCS, vol. 8552, pp. 93\u2013109. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12466-7_6"},{"doi-asserted-by":"publisher","unstructured":"Kersten, R., Shkaravska, O., van Gastel, B., Montenegro, M., Eekelenvan Eekelen, M.: Making resource analysis practical for real-time Java. In: Proceedings of JTRES 2012, pp. 135\u2013144. ACM (2012). https:\/\/doi.org\/10.1145\/2388936.2388959","key":"3_CR17","DOI":"10.1145\/2388936.2388959"},{"issue":"7","key":"3_CR18","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)","journal-title":"Commun. ACM"},{"doi-asserted-by":"crossref","unstructured":"Klinik, M., van Gastel, B., Kop, C., Eekelenvan Eekelen, M.: Skylines for symbolic energy consumption analysis - technical report. Technical report, Radboud University (2020). https:\/\/gitlab.science.ru.nl\/mklinik\/eca-symbolic-execution\/blob\/master\/paper\/techreport.pdf","key":"3_CR19","DOI":"10.1007\/978-3-030-58298-2_3"},{"doi-asserted-by":"crossref","unstructured":"Klinik, M., Jansen, J.M., Plasmeijer, R.: The sky is the limit: analysing resource consumption over time using skylines. In: Proceedings of the 29th Symposium on Implementation and Application of Functional Programming Languages, IFL 2017. ACM (2017)","key":"3_CR20","DOI":"10.1145\/3205368.3205376"},{"unstructured":"Microchip Technology Inc.: ATmega48A\/PA\/88A\/PA\/168A\/PA\/328\/P Data Sheet (2018)","key":"3_CR21"},{"key":"3_CR22","volume-title":"Semantics With Applications: A Formal Introduction","author":"HR Nielson","year":"1992","unstructured":"Nielson, H.R., Nielson, F.: Semantics With Applications: A Formal Introduction. Wiley, Hoboken (1992)"},{"issue":"1","key":"3_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1155\/2011\/316510","volume":"2011","author":"B Nogueira","year":"2011","unstructured":"Nogueira, B., Maciel, P., Tavares, E., Andrade, E., Massa, R., Callou, G., Ferraz, R.: A formal model for performance and energy evaluation of embedded systems. EURASIP J. Embed. Syst. 2011(1), 1\u201312 (2011). https:\/\/doi.org\/10.1155\/2011\/316510","journal-title":"EURASIP J. Embed. Syst."},{"issue":"4","key":"3_CR24","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/1721654.1721673","volume":"53","author":"P Ranganathan","year":"2010","unstructured":"Ranganathan, P.: Recipe for efficiency: principles of power-aware computing. Commun. ACM 53(4), 60\u201367 (2010)","journal-title":"Commun. ACM"},{"issue":"6","key":"3_CR25","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1145\/1993316.1993518","volume":"46","author":"A Sampson","year":"2011","unstructured":"Sampson, A., Dietl, W., Fortuna, E., Gnanapragasam, D., Ceze, L., Grossman, D.: EnerJ: approximate data types for safe and general low-power computation. SIGPLAN Not. 46(6), 164\u2013174 (2011)","journal-title":"SIGPLAN Not."},{"issue":"2","key":"3_CR26","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/1646353.1646370","volume":"53","author":"E Saxe","year":"2010","unstructured":"Saxe, E.: Power-efficient software. Commun. ACM 53(2), 44\u201348 (2010). https:\/\/doi.org\/10.1145\/1646353.1646370","journal-title":"Commun. ACM"},{"doi-asserted-by":"crossref","unstructured":"Sinha, A., Chandrakasan, A.P.: JouleTrack: a web based tool for software energy profiling. In: Proceedings of DAC 2001, pp. 220\u2013225. ACM (2001)","key":"3_CR27","DOI":"10.1145\/378239.378467"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58298-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T06:02:53Z","timestamp":1707458573000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-58298-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030582975","9783030582982"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58298-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"29 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vienna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fmics20.ait.ac.at\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"42% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}