{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T03:12:01Z","timestamp":1772593921113,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030636173","type":"print"},{"value":"9783030636180","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/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":"http:\/\/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-63618-0_6","type":"book-chapter","created":{"date-parts":[[2020,12,5]],"date-time":"2020-12-05T08:04:14Z","timestamp":1607155454000},"page":"87-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8262-2919","authenticated-orcid":false,"given":"Alessandro","family":"Trindade","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6235-4272","authenticated-orcid":false,"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,12,6]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-63387-9_23","volume-title":"Computer Aided Verification","author":"A Abate","year":"2017","unstructured":"Abate, A., et al.: Automated formal synthesis of digital controllers for state-space physical plants. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 462\u2013482. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_23"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-54292-8_1","volume-title":"Numerical Software Verification","author":"A Abate","year":"2017","unstructured":"Abate, A.: Verification of networks of smart energy systems over the cloud. In: Bogomolov, S., Martel, M., Prabhakar, P. (eds.) NSV 2016. LNCS, vol. 10152, pp. 1\u201314. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-54292-8_1"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-96145-3_15","volume-title":"Computer Aided Verification","author":"A Abate","year":"2018","unstructured":"Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 270\u2013288. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_15"},{"issue":"1761","key":"6_CR4","first-page":"1","volume":"8","author":"S Alsadi","year":"2018","unstructured":"Alsadi, S., Khatib, T.: Photovoltaic power systems optimization research status: a review of criteria, constrains, models, techniques, and software tools. Appl. Sci. 8(1761), 1\u201330 (2018)","journal-title":"Appl. Sci."},{"issue":"1","key":"6_CR5","doi-asserted-by":"publisher","first-page":"76","DOI":"10.18178\/ijeee.5.1.76-83","volume":"5","author":"S Barua","year":"2017","unstructured":"Barua, S., Prasath, R.A., Boruah, D.: Rooftop solar photovoltaic system design and assessment for the academic campus using PVsyst software. Int. J. Electron. Electr. Eng. 5(1), 76\u201383 (2017)","journal-title":"Int. J. Electron. Electr. Eng."},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: $${\\nu }Z$$ - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_14"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-10575-8_1","volume-title":"In: Handbook of Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H.: Introduction to model checking. In: Handbook of Model Checking, pp. 1\u201326. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_1"},{"key":"6_CR11","unstructured":"Coelho, S., et al.: Biomass residues as electricity generation source in low HD source in regions of Brazil. In: UNESP (ed.) The XI Latin Congress of Electricity Generation and Transmission - CLAGTEE, pp. 1\u20138 (2015)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Driouich, Y., Parente, M., Tronci, E.: A methodology for a complete simulation of cyber-physical energy systems. In: IEEE Workshop on Environmental, Energy, and Structural Monitoring Systems (EESMS), pp. 1\u20135 (2018)","DOI":"10.1109\/EESMS.2018.8405826"},{"key":"6_CR13","unstructured":"Empresa de Pesquisa Energ\u00e9tica EPE: Sistemas Isolados - Planejamento Ciclo 2018\u20132023 (2018). http:\/\/www.epe.gov.br\/sites-pt\/publicacoes-dados-abertos\/publicacoes. Accessed 04 Apr 2019"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Gadelha, M., Monteiro, F., Morse, J., Cordeiro, L., Fischer, B., Nicole, D.: ESBMC 5.0: an industrial-strength C model checker. In: 33rd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2018), pp. 888\u2013891. ACM, New York (2018)","DOI":"10.1145\/3238147.3240481"},{"key":"6_CR15","unstructured":"Gadelha, M.Y.R., Cordeiro, L.C., Nicole, D.A.: An efficient floating-point bit-blasting API for verifying C programs. CoRR abs\/2004.12699 (2020). https:\/\/arxiv.org\/abs\/2004.12699"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Gow, J., Manning, C.: Development of a photovoltaic array model for use in power-electronics simulation studies. In: Proceedings of the 14th IEE Electric Power Applications Conference, vol. 146(2), pp. 193\u2013200 (1999)","DOI":"10.1049\/ip-epa:19990116"},{"key":"6_CR17","unstructured":"Hansen, A., S\u00f8rensen, P., Hansen, L., Bindner, H.: Models for a stand-alone PV system. No. 1219 in Denmark. Forskningscenter Risoe. Risoe-r, Forskningscenter Risoe (2001)"},{"key":"6_CR18","unstructured":"HOMER: The HOMER microgrid software (2017). http:\/\/www.homerenergy.com\/software.html. Accessed 1 June 2019"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Hussein, M., Leal Filho, W.: Analysis of energy as a precondition for improvement of living conditions and poverty reduction in sub-Saharan Africa. In: Scientific Research and Essays, vol. 7(30), pp. 2656\u20132666 (2012)","DOI":"10.5897\/SRE11.929"},{"key":"6_CR20","unstructured":"IEA: World Energy Outlook 2018. IEA, Paris (2018)"},{"key":"6_CR21","unstructured":"Karekesi, S., Lata, K., Coelho, S.: Renewable Energy - A Global Review of Technologies, Policies and Markets, chap. Traditional Biomass Energy: Improving Its Use and Moving to Modern Energy Use, pp. 231\u2013261. Earthscan, London (2006)"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Khatib, T., Elmenreich, W.: Optimum availability of standalone photovoltaic power systems for remote housing electrification. Int. J. Photoenergy 2014(Article ID 475080), 5 pages (2014)","DOI":"10.1155\/2014\/475080"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 c bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"6_CR24","volume-title":"Manual de Engenharia para Sistemas Fotovoltaicos","author":"J Pinho","year":"2014","unstructured":"Pinho, J., Galdino, M.: Manual de Engenharia para Sistemas Fotovoltaicos. CEPEL - CRESESB, Rio de Janeiro (2014)"},{"issue":"4","key":"6_CR25","first-page":"203","volume":"4","author":"S Pradhan","year":"2015","unstructured":"Pradhan, S., Singh, S., Choudhury, M., Dwivedy, D.: Study of cost analysis and emission analysis for grid connected PV systems using RETSCREEN 4 simulation software. Int. J. Eng. Res. Tech. 4(4), 203\u2013207 (2015)","journal-title":"Int. J. Eng. Res. Tech."},{"key":"6_CR26","unstructured":"PVsyst: Logiciel Photovolta\u00efque (2020). https:\/\/www.pvsyst.com\/. Accessed 24 Apr 2020"},{"issue":"5","key":"6_CR27","doi-asserted-by":"publisher","first-page":"2077","DOI":"10.1109\/TPWRD.2014.2376571","volume":"30","author":"A Sengupta","year":"2015","unstructured":"Sengupta, A., Mukhopadhyay, S., Sinha, A.: Automated verification of power system protection schemes\u2013Part I: modeling and specifications. IEEE Tran. Power Del. 30(5), 2077\u20132086 (2015)","journal-title":"IEEE Tran. Power Del."},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Swarnkar, N., Gidwani, L., Sharma, R.: An application of HOMER Pro in optimization of hybrid energy system for electrification of technical institute. In: International Conference on Energy Efficient Technologies for Sustainability (ICEETS), pp. 56\u201361 (2016)","DOI":"10.1109\/ICEETS.2016.7582899"},{"key":"6_CR29","unstructured":"Trindade, A.: Ferramenta de an\u00e1lise comparativa de projetos de eletrifica\u00e7\u00e3o rural com fontes renov\u00e1veis de energia na amaz\u00f4nia. In: IX Congresso sobre Gera\u00e7\u00e3o Distribu\u00edda e Energia no Meio Rural - AGRENER GD. p. n.pag. (2013)"},{"key":"6_CR30","unstructured":"Trindade, A., Cordeiro, L.C.: Optimal sizing of stand-alone solar PV systems via automated formal synthesis. CoRR abs\/1909.13139 (2019). http:\/\/arxiv.org\/abs\/1909.13139"},{"issue":"1","key":"6_CR31","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1016\/j.solener.2019.09.093","volume":"193","author":"AB Trindade","year":"2019","unstructured":"Trindade, A.B., Cordeiro, L.C.: Automated formal verification of stand-alone solar photovoltaic systems. Solar Energy 193(1), 684\u2013691 (2019)","journal-title":"Solar Energy"},{"issue":"6","key":"6_CR32","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1504\/IJES.2017.088044","volume":"9","author":"AB Trindade","year":"2017","unstructured":"Trindade, A.B., Degelo, R.D.F., Junior, E.G.D.S., Ismail, H.I., Silva, H.C.D., Cordeiro, L.C.: Multi-core model checking and maximum satisfiability applied to hardware-software partitioning. IJES 9(6), 570\u2013582 (2017)","journal-title":"IJES"}],"container-title":["Lecture Notes in Computer Science","Software Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-63618-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T12:24:59Z","timestamp":1619267099000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-63618-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030636173","9783030636180"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-63618-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"6 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"19 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sri-csl.github.io\/VSTTE20\/","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":"7","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":"4","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":"57% - 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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to COVID-19 pandemic the conference was held virtually","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)"}}]}}