{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T10:42:27Z","timestamp":1748083347405,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452339"},{"type":"electronic","value":"9783030452346"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45234-6_22","type":"book-chapter","created":{"date-parts":[[2020,4,20]],"date-time":"2020-04-20T14:04:23Z","timestamp":1587391463000},"page":"441-461","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8108-0043","authenticated-orcid":false,"given":"Aren A.","family":"Babikian","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3592-5105","authenticated-orcid":false,"given":"Oszk\u00e1r","family":"Semer\u00e1th","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8790-252X","authenticated-orcid":false,"given":"D\u00e1niel","family":"Varr\u00f3","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"22_CR1","unstructured":"Viatra solver project. \nhttps:\/\/github.com\/viatra\/VIATRA-Generator"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Ali, S., Iqbal, M.Z., Khalid, M., Arcuri, A.: Improving the performance of OCL constraint solving with novel heuristics for logical operations: a search-based approach. Empirical Software Engineering 21(6), 2459\u20132502 (Dec 2016). \nhttps:\/\/doi.org\/10.1007\/s10664-015-9392-6","DOI":"10.1007\/s10664-015-9392-6"},{"key":"22_CR3","doi-asserted-by":"publisher","unstructured":"Atkinson, T., Plump, D., Stepney, S.: Evolving graphs by graph programming. In: Genetic Programming - 21st European Conference, EuroGP 2018, Parma, Italy, April 4-6, 2018, Proceedings. LNCS, vol. 10781, pp. 35\u201351. Springer (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-77553-1_3","DOI":"10.1007\/978-3-319-77553-1_3"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Atkinson, T., Plump, D., Stepney, S.: Evolving graphs with horizontal gene transfer. In: Proceedings of the Genetic and Evolutionary Computation Conference, GECCO 2019, Prague, Czech Republic, July 13-17, 2019. pp. 968\u2013976. ACM (2019). \nhttps:\/\/doi.org\/10.1145\/3321707.3321788","DOI":"10.1145\/3321707.3321788"},{"key":"22_CR5","doi-asserted-by":"publisher","unstructured":"Bagan, G., Bonifati, A., Ciucanu, R., Fletcher, G.H.L., Lemay, A., Advokaat, N.: gmark: Schema-driven generation of graphs and queries. IEEE Trans. Knowl. Data Eng. 29(4), 856\u2013869 (2017). \nhttps:\/\/doi.org\/10.1109\/TKDE.2016.2633993","DOI":"10.1109\/TKDE.2016.2633993"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Wolff, B.: HOL-OCL: A formal proof environment for UML\/OCL. In: Fiadeiro, J.L., Inverardi, P. (eds.) Fundamental Approaches to Software Engineering. pp. 97\u2013100. Springer, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78743-3_8"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: ICFEM. pp. 198\u2013213. Springer (2012)","DOI":"10.1007\/978-3-642-34281-3_16"},{"key":"22_CR8","doi-asserted-by":"publisher","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: On the verification of UML\/OCL class diagrams using constraint programming. Journal of Systems and Software (Mar 2014). \nhttps:\/\/doi.org\/10.1016\/j.jss.2014.03.023","DOI":"10.1016\/j.jss.2014.03.023"},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Gogolla, M., B\u00fcttner, F., Richters, M.: USE: A UML-based specification environment for validating UML and OCL. Science of Computer Programming 69(1), 27 \u2013 34 (2007). \nhttps:\/\/doi.org\/10.1016\/j.scico.2007.01.013","DOI":"10.1016\/j.scico.2007.01.013"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez P\u00e9rez, C.A., Buettner, F., Claris\u00f3, R., Cabot, J.: EMFtoCSP: A Tool for the Lightweight Verification of EMF Models. In: Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA). Zurich, Switzerland (Jun 2012), \nhttps:\/\/hal.inria.fr\/hal-00688039","DOI":"10.1109\/FormSERA.2012.6229788"},{"key":"22_CR11","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York, NY, USA (1993)"},{"key":"22_CR12","unstructured":"Hao, W.: Automated metamodel instance generation satisfying quantitative constraints. Ph.D. thesis, National University of Ireland Maynooth (2013)"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002). \nhttps:\/\/doi.org\/10.1145\/505145.505149","DOI":"10.1145\/505145.505149"},{"key":"22_CR14","unstructured":"Jackson, D.: Software Abstractions: logic, language, and analysis. MIT press (2012)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: Model Driven Engineering Languages and Systems, pp. 653\u2013667. Springer (2011)","DOI":"10.1007\/978-3-642-24485-8_48"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Jackson, E.K., Sztipanovits, J.: Towards a formal foundation for domain specific modeling languages. In: EMSOFT. pp. 53\u201362. ACM, New York, NY, USA (2006)","DOI":"10.1145\/1176887.1176896"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Juneau, J.: Object Relational Mapping and JPA, pp. 55\u201372. Apress, Berkeley, CA (2013)","DOI":"10.1007\/978-1-4302-5849-0_4"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Khurshid, S., Marinov, D.: Testera: Specification-based testing of java programs using SAT. Autom. Softw. Eng. 11(4), 403\u2013434 (2004). \nhttps:\/\/doi.org\/10.1023\/B:AUSE.0000038938.10589.b9","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044. pp. 1\u201335. CAV 2013, Springer-Verlag, New York, NY, USA (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S.: Korat: A tool for generating structurally complex test inputs. In: ICSE. pp. 771\u2013774. IEEE Computer Society (2007). \nhttps:\/\/doi.org\/10.1109\/ICSE.2007.48","DOI":"10.1109\/ICSE.2007.48"},{"key":"22_CR21","doi-asserted-by":"publisher","unstructured":"Miller, J.F.: Cartesian genetic programming: its status and future. Genetic Programming and Evolvable Machines (2019). \nhttps:\/\/doi.org\/10.1007\/s10710-019-09360-6","DOI":"10.1007\/s10710-019-09360-6"},{"key":"22_CR22","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. pp. 337\u2013340 (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Navarro, J.A., Voronkov, A.: Proof systems for effectively propositional logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning. pp. 426\u2013440. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-71070-7_36"},{"key":"22_CR24","unstructured":"The Object Management Group: Object Constraint Language, v2.4 (February 2014)"},{"key":"22_CR25","doi-asserted-by":"publisher","unstructured":"Schneider, S., Lambers, L., Orejas, F.: Symbolic model generation for graph properties. In: Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. pp. 226\u2013243 (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54494-5_13","DOI":"10.1007\/978-3-662-54494-5_13"},{"key":"22_CR26","doi-asserted-by":"publisher","unstructured":"Schneider, S., Lambers, L., Orejas, F.: Automated reasoning for attributed graph properties. STTT 20(6), 705\u2013737 (2018). \nhttps:\/\/doi.org\/10.1007\/s10009-018-0496-3","DOI":"10.1007\/s10009-018-0496-3"},{"key":"22_CR27","unstructured":"Semer\u00e1th, O., Babikian, A.A., Pilarski, S., Varr\u00f3, D.: VIATRA Solver: a framework for the automated generation of consistent domain-specific models. In: ICSE. pp. 43\u201346 (2019), \nhttps:\/\/dl.acm.org\/citation.cfm?id=3339687"},{"key":"22_CR28","doi-asserted-by":"publisher","unstructured":"Semer\u00e1th, O., Barta, \u00c1., Horv\u00e1th, \u00c1., Szatm\u00e1ri, Z., Varr\u00f3, D.: Formal validation of domain-specific languages with derived features and well-formedness constraints. Software and Systems Modeling pp. 357\u2013392 (2017). \nhttps:\/\/doi.org\/10.1016\/j.entcs.2008.04.038","DOI":"10.1016\/j.entcs.2008.04.038"},{"key":"22_CR29","doi-asserted-by":"publisher","unstructured":"Semer\u00e1th, O., Farkas, R., Bergmann, G., Varr\u00f3, D.: Diversity of graph models and graph generators in mutation testing. STTT 22(1), 57\u201378 (2020). \nhttps:\/\/doi.org\/10.1007\/s10009-019-00530-6","DOI":"10.1007\/s10009-019-00530-6"},{"key":"22_CR30","doi-asserted-by":"publisher","unstructured":"Semer\u00e1th, O., Nagy, A.S., Varr\u00f3, D.: A graph solver for the automated generation of consistent domain-specific models. In: ICSE. pp. 969\u2013980. ACM (2018). \nhttps:\/\/doi.org\/10.1145\/3180155.3180186","DOI":"10.1145\/3180155.3180186"},{"key":"22_CR31","doi-asserted-by":"publisher","unstructured":"Soltana, G., Sabetzadeh, M., Briand, L.C.: Synthetic data generation for statistical testing. In: ASE. pp. 872\u2013882 (2017). \nhttps:\/\/doi.org\/10.1109\/ASE.2017.8115698","DOI":"10.1109\/ASE.2017.8115698"},{"key":"22_CR32","unstructured":"Soltana, G., Sabetzadeh, M., Briand, L.C.: Practical model-driven data generation for system testing. CoRR abs\/1902.00397 (2019)"},{"key":"22_CR33","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. Journal of Automated Reasoning 59(4), 483\u2013502 (Dec 2017). \nhttps:\/\/doi.org\/10.1007\/s10817-017-9407-7","DOI":"10.1007\/s10817-017-9407-7"},{"key":"22_CR34","doi-asserted-by":"publisher","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: TACAS. LNCS, vol. 4424, pp. 632\u2013647. Springer (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71209-1_49","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"22_CR35","doi-asserted-by":"publisher","unstructured":"Ujhelyi, Z., Bergmann, G., Heged\u00fcs, \u00c1., Horv\u00e1th, \u00c1., Izs\u00f3, B., R\u00e1th, I., Szatm\u00e1ri, Z., Varr\u00f3, D.: EMF-IncQuery: An integrated development environment for live model queries. Sci. Comput. Program. 98, 80\u201399 (2015). \nhttps:\/\/doi.org\/10.1016\/j.scico.2014.01.004","DOI":"10.1016\/j.scico.2014.01.004"},{"key":"22_CR36","doi-asserted-by":"crossref","unstructured":"Varr\u00f3, D., Bergmann, G., Heged\u00fcs, \u00c1., Horv\u00e1th, \u00c1., R\u00e1th, I., Ujhelyi, Z.: Road to a reactive and incremental model transformation platform: three generations of the VIATRA framework. Software and Systems Modeling 15(3), 609\u2013629 (2016)","DOI":"10.1007\/s10270-016-0530-4"},{"key":"22_CR37","doi-asserted-by":"publisher","unstructured":"Varr\u00f3, D., Semer\u00e1th, O., Sz\u00e1rnyas, G., Horv\u00e1th, \u00c1.: Towards the automated generation of consistent, diverse, scalable and realistic graph models. In: Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig. LNCS, vol. 10800, pp. 285\u2013312. Springer (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-75396-6_16","DOI":"10.1007\/978-3-319-75396-6_16"},{"key":"22_CR38","doi-asserted-by":"publisher","unstructured":"Wu, H., Monahan, R., Power, J.F.: Exploiting attributed type graphs to generate metamodel instances using an SMT solver. In: TASE. pp. 175\u2013182 (July 2013). \nhttps:\/\/doi.org\/10.1109\/TASE.2013.31","DOI":"10.1109\/TASE.2013.31"},{"key":"22_CR39","unstructured":"Yakindu Statechart Tools: Yakindu (2019), \nhttp:\/\/statecharts.org\/"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45234-6_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,11]],"date-time":"2020-08-11T12:23:24Z","timestamp":1597148604000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45234-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452339","9783030452346"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45234-6_22","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":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","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":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"81","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":"23","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":"28% - 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":"9","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 could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","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)"}}]}}