{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:36:35Z","timestamp":1742913395525,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319498140"},{"type":"electronic","value":"9783319498157"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","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":[[2016]]},"DOI":"10.1007\/978-3-319-49815-7_9","type":"book-chapter","created":{"date-parts":[[2016,11,12]],"date-time":"2016-11-12T09:12:09Z","timestamp":1478941929000},"page":"145-160","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["An Evolutionary Approach to Translate Operational Specifications into Declarative Specifications"],"prefix":"10.1007","author":[{"given":"Facundo","family":"Molina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9sar","family":"Cornejo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Renzo","family":"Degiovanni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Germ\u00e1n","family":"Regis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pablo F.","family":"Castro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,13]]},"reference":[{"key":"9_CR1","unstructured":"Bicarregui, J., Bishop, M., Dimitrakos, T., Lano, K., Maibaum, T., Matthews, B., Ritchie, B.: Supporting co-use of VDM and B by translation. In: Proceedings of VDM in 2000! (2nd VDM workshop) (2000)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: Proceedings of the 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2002. ACM (2002)","DOI":"10.1145\/566172.566191"},{"issue":"3","key":"9_CR3","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of JML tools and applications. STTT 7(3), 212\u2013232 (2005). Springer","journal-title":"STTT"},{"issue":"28","key":"9_CR4","doi-asserted-by":"publisher","first-page":"3129","DOI":"10.1016\/j.tcs.2011.02.034","volume":"412","author":"S Cranen","year":"2011","unstructured":"Cranen, S., Groote, J.F., Reniers, M.: A linear translation from CTL* to the first-order modal mu-calculus. Theor. Comput. Sci. 412(28), 3129\u20133139 (2011). Elsevier","journal-title":"Theor. Comput. Sci."},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-319-02444-8_13","volume-title":"Automated Technology for Verification and Analysis","author":"R Demasi","year":"2013","unstructured":"Demasi, R., Castro, P.F., Maibaum, T.S.E., Aguirre, N.: Synthesizing masking fault-tolerant systems from deontic specifications. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 163\u2013177. Springer, Heidelberg (2013). doi:\n                      10.1007\/978-3-319-02444-8_13"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1007\/978-3-642-24372-1_41","volume-title":"Automated Technology for Verification and Analysis","author":"EA Emerson","year":"2011","unstructured":"Emerson, E.A., Samanta, R.: An algorithmic framework for synthesis of concurrent programs. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 522\u2013530. Springer, Heidelberg (2011). doi:\n                      10.1007\/978-3-642-24372-1_41"},{"issue":"1\u20133","key":"9_CR7","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007). Elsevier","journal-title":"Sci. Comput. Program."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: upgrading alloy with actions. In: Proceedings of International Conference on Software Engineering, ICSE 2005. ACM (2015)","DOI":"10.1145\/1062455.1062535"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., L\u00f3pez Pombo, C., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA 2010. ACM (2010)","DOI":"10.1145\/1831708.1831712"},{"issue":"9","key":"9_CR10","doi-asserted-by":"publisher","first-page":"1283","DOI":"10.1109\/TSE.2013.15","volume":"39","author":"JP Galeotti","year":"2013","unstructured":"Galeotti, J.P., Rosner, N., Pombo, C.L., Frias, M.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Softw. Eng. 39(9), 1283\u20131307 (2013). IEEE","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"10","key":"9_CR11","doi-asserted-by":"publisher","first-page":"1019","DOI":"10.1109\/TSE.2015.2431688","volume":"41","author":"JP Galeotti","year":"2015","unstructured":"Galeotti, J.P., Furia, C.A., May, E., Fraser, G., Zeller, A.: Inferring loop invariants by mutation, dynamic analysis, and static checking. IEEE Trans. Softw. Eng. 41(10), 1019\u20131037 (2015). IEEE","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR12","volume-title":"Fundamentals of Software Engineering","author":"C Ghezzi","year":"2003","unstructured":"Ghezzi, C., Jazayeri, M., Mandiroli, D.: Fundamentals of Software Engineering, 2nd edn. Prentice-Hall, Upper Saddle River (2003)","edition":"2"},{"key":"9_CR13","volume-title":"Genetic Algorithms in Search, Optimization and Machine Learning","author":"D Goldberg","year":"1989","unstructured":"Goldberg, D.: Genetic Algorithms in Search, Optimization and Machine Learning. Addison-Wesley, Salt Lake City (1989)"},{"key":"9_CR14","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"9_CR15","unstructured":"Web site of the Java Genetic Algorithms Package (JGAP). \n                      http:\/\/jgap.sourceforge.net"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-642-27940-9_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"U Klein","year":"2012","unstructured":"Klein, U., Piterman, N., Pnueli, A.: Effective synthesis of asynchronous systems from GR(1) specifications. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 283\u2013298. Springer, Heidelberg (2012). doi:\n                      10.1007\/978-3-642-27940-9_19"},{"key":"9_CR17","unstructured":"Home Page of the Korat test generation tool. \n                      http:\/\/korat.sourceforge.net"},{"key":"9_CR18","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). doi:\n                      10.1007\/978-3-642-54862-8_26"},{"key":"9_CR19","volume-title":"Program Development in Java: Abstraction, Specification, and Object-Oriented Desig","author":"B Liskov","year":"2000","unstructured":"Liskov, B., Guttag, J.: Program Development in Java: Abstraction, Specification, and Object-Oriented Desig. Addison-Wesley, Salt Lake City (2000)"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Michalewicz, Z.: Genetic Algorithms + Data Structures = Evolution Programs, Springer, Heidelberg (1996)","DOI":"10.1007\/978-3-662-03315-9"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: Proceedings of the 29th International Conference on Software Engineering, ICSE 2007. IEEE (2007)","DOI":"10.1109\/ICSE.2007.37"},{"issue":"3","key":"9_CR22","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"CS Pasareanu","year":"2008","unstructured":"Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. 32(3), 175\u2013205 (2008). Springer","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Ponzio, P., Aguirre, N., Frias, M., Visser, W.: Field-exhaustive testing. In: Proceedings of International Symposium on the Foundations of Software Engineering FSE 2016, Seattle (WA), USA. ACM (2016, to appear)","DOI":"10.1145\/2950290.2950336"},{"key":"9_CR24","volume-title":"Artificial Intelligence: A Modern Approach","author":"S Russell","year":"2003","unstructured":"Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Prentice-Hall, Upper Saddle River (2003)","edition":"2"},{"issue":"3","key":"9_CR25","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1109\/TSE.2008.107","volume":"35","author":"S Uchitel","year":"2009","unstructured":"Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Softw. Eng. 35(3), 384\u2013406 (2009). IEEE","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004. ACM (2004)","DOI":"10.1145\/1007512.1007526"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-49815-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:40:08Z","timestamp":1558316408000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-49815-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319498140","9783319498157"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-49815-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Natal","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 November 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sbmf2016.imd.ufrn.br\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}