{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:52Z","timestamp":1740099172501,"version":"3.37.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030021481"},{"type":"electronic","value":"9783030021498"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-030-02149-8_20","type":"book-chapter","created":{"date-parts":[[2018,10,5]],"date-time":"2018-10-05T17:25:34Z","timestamp":1538760334000},"page":"333-349","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Set Solver for Finite Set Relation Algebra"],"prefix":"10.1007","author":[{"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[]},{"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,6]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"issue":"604","key":"20_CR2","doi-asserted-by":"publisher","first-page":"0","DOI":"10.1090\/memo\/0604","volume":"126","author":"Hajnal Andr\u00e9ka","year":"1997","unstructured":"Andr\u00e9ka, H., Givant, S.R., N\u00e9meti, I.: Decision Problems for Equational Theories of Relation Algebras, vol. 604. American Mathematical Society, Providence (1997)","journal-title":"Memoirs of the American Mathematical Society"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-39634-2_16","volume-title":"Interactive Theorem Proving","author":"A Armstrong","year":"2013","unstructured":"Armstrong, A., Struth, G., Weber, T.: Program analysis and verification based on Kleene algebra in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 197\u2013212. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_16"},{"key":"20_CR4","unstructured":"Berghammer, R.: Relview. http:\/\/www.informatik.uni-kiel.de\/~progsys\/relview\/"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-06251-8_11","volume-title":"Relational and Algebraic Methods in Computer Science","author":"R Berghammer","year":"2014","unstructured":"Berghammer, R., H\u00f6fner, P., Stucke, I.: Automated verification of relational while-programs. In: H\u00f6fner, P., Jipsen, P., Kahl, W., M\u00fcller, M.E. (eds.) RAMiCS 2014. LNCS, vol. 8428, pp. 173\u2013190. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06251-8_11"},{"key":"20_CR6","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroc\u0142aw, Poland, August 2011. http:\/\/proval.lri.fr\/submissions\/boogie11.pdf"},{"key":"20_CR7","doi-asserted-by":"publisher","unstructured":"Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Log. Methods Comput. 8(1), 1\u201342 (2012). https:\/\/doi.org\/10.2168\/LMCS-8(1:16)2012","DOI":"10.2168\/LMCS-8(1:16)2012"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-33951-1_18","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"S Conchon","year":"2016","unstructured":"Conchon, S., Iguernlala, M.: Increasing proofs automation rate of Atelier-B thanks to Alt-Ergo. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 243\u2013253. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33951-1_18"},{"key":"20_CR9","unstructured":"Cristi\u00e1, M., Rossi, G.: Rewrite rules for a solver for sets, binary relations and partial functions. http:\/\/people.dmi.unipr.it\/gianfranco.rossi\/SETLOG\/calculus.pdf"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-41528-4_10","volume-title":"Computer Aided Verification","author":"M Cristi\u00e1","year":"2016","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for sets, binary relations and partial functions. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 179\u2013198. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_10"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-319-63046-5_12","volume-title":"Automated Deduction \u2013 CADE 26","author":"Maximiliano Cristi\u00e1","year":"2017","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura [26], pp. 185\u2013201. https:\/\/doi.org\/10.1007\/978-3-319-63046-5_12"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M., Rossi, G.: A set solver for finite relation algebra - extended version. Technical report (2018). https:\/\/www.researchgate.net\/publication\/320555347_A_Set_Solver_for_Finite_Relation_Algebra","DOI":"10.1007\/978-3-030-02149-8_20"},{"key":"20_CR13","doi-asserted-by":"publisher","unstructured":"Deters, M., Reynolds, A., King, T., Barrett, C.W., Tinelli, C.: A tour of CVC4: how it works, and how to use it. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 October 2014, p. 7. IEEE (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987586","DOI":"10.1109\/FMCAD.2014.6987586"},{"issue":"5","key":"20_CR14","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1145\/365151.365169","volume":"22","author":"A Dovier","year":"2000","unstructured":"Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861\u2013931 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Dovier, A., Policriti, A., Rossi, G.: A uniform axiomatic view of lists, multisets, and sets, and the relevant unification algorithms. Fundam. Inform. 36(2\u20133), 201\u2013234 (1998). https:\/\/doi.org\/10.3233\/FI-1998-36235","DOI":"10.3233\/FI-1998-36235"},{"issue":"06","key":"20_CR16","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1017\/S1471068406002730","volume":"6","author":"AGOSTINO DOVIER","year":"2006","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log. Prog. 6(6), 645\u2013701 (2006). https:\/\/doi.org\/10.1017\/S1471068406002730","journal-title":"Theory and Practice of Logic Programming"},{"issue":"4","key":"20_CR17","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10817-006-9062-x","volume":"37","author":"Steven Givant","year":"2007","unstructured":"Givant, S.: The calculus of relations as a foundation for mathematics. J. Autom. Reasoning 37(4), 277\u2013322 (2006). https:\/\/doi.org\/10.1007\/s10817-006-9062-x","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR18","unstructured":"Guttmann, W., Struth, G., Weber, T.: A repository for Tarski-Kleene algebras. In: H\u00f6fner, P., McIver, A., Struth, G. (eds.) Proceedings of the First Workshop on Automated Theory Engineering, Wroc\u0142aw, Poland, 31 July 2011. CEUR Workshop Proceedings, vol. 760, pp. 30\u201339. CEUR-WS.org (2011). http:\/\/ceur-ws.org\/Vol-760\/paper5.pdf"},{"key":"20_CR19","unstructured":"Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf: The ProB animator and model checker. https:\/\/www3.hhu.de\/stups\/prob\/index.php\/Main_Page"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71070-7_5","volume-title":"Automated Reasoning","author":"P H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P., Struth, G.: On automating the calculus of relations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 50\u201366. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_5"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44880-2_1","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"D Jackson","year":"2003","unstructured":"Jackson, D.: Alloy: a logical modelling language. In: Bert, D., Bowen, J.P., King, S., Wald\u00e9n, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 1\u20131. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44880-2_1"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"key":"20_CR23","unstructured":"Maddux, R.: Relation Algebras, vol. 13. Elsevier (2006). https:\/\/books.google.it\/books?id=fjFH1WvPG9AC"},{"key":"20_CR24","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"20_CR25","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-63046-5_10","volume-title":"Automated Deduction \u2013 CADE 26","author":"Baoluo Meng","year":"2017","unstructured":"Meng, B., Reynolds, A., Tinelli, C., Barrett, C.W.: Relational constraint solving in SMT. In: de Moura [26], pp. 148\u2013165. https:\/\/doi.org\/10.1007\/978-3-319-63046-5_10"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5","volume-title":"Automated Deduction \u2013 CADE 26","year":"2017","unstructured":"de Moura, L. (ed.): Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, 6\u201311 August 2017, Proceedings. LNCS, vol. 10395. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"20_CR28","unstructured":"Rossi, G.: $$\\{log\\}$$ (2008). http:\/\/people.dmi.unipr.it\/gianfranco.rossi\/setlog.Home.html"},{"key":"20_CR29","unstructured":"Saaltink, M.: The Z\/EVES mathematical toolkit version 2.2 for Z\/EVES version 1.5. Technical report, ORA Canada (1997)"},{"key":"20_CR30","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-7091-6510-2_3","volume-title":"Relational Methods in Computer Science","author":"Gunther Schmidt","year":"1997","unstructured":"Schmidt, G., Hattensperger, C., Winter, M.: Heterogeneous Relation Algebra, pp. 39\u201353. Springer, Vienna (1997). https:\/\/doi.org\/10.1007\/978-3-7091-6510-2_3"},{"key":"20_CR31","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., Hertfordshire (1992)"},{"issue":"4","key":"20_CR32","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF Parts, v3.5.0. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"03","key":"20_CR33","doi-asserted-by":"publisher","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"Alfred Tarski","year":"1941","unstructured":"Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73\u201389 (1941). https:\/\/doi.org\/10.2307\/2268577","journal-title":"The Journal of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02149-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,25]],"date-time":"2019-10-25T11:07:50Z","timestamp":1572001670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02149-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030021481","9783030021498"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02149-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"RAMiCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Relational and Algebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Groningen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 November 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ramics2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.ramics-conference.org\/","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"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"70% - 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"}},{"value":"4.06","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"4.17","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"1 full invited talk","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}