{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:02:40Z","timestamp":1743084160981,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Rewriting Modulo SMT combines two powerful automated deduction techniques (1) rewriting and (2) SMT-solving. Rewriting enables the specification of behavior of systems using rewriting rules, while SMT theories specify system properties. Rewriting Modulo SMT is enabled by combining existing tools, such as Maude and SMT solvers. Search algorithms used for carrying out Rewriting Modulo SMT, however, cannot exploit the incremental solving features available in SMT solvers as they are based on breadth-first search. This paper addresses this limitation by proposing Incremental Rewriting Modulo SMT Theories, which is a syntactical restriction to rewriting rules. This restriction turns out to naturally be used in several applications of Rewriting Modulo SMT, including the verification of algorithms, cyber-physical systems, and security protocols. Moreover, we propose a Hybrid-Search algorithm for Incremental Rewriting Modulo SMT Theories that combines breadth-first search and depth-first search, thus enabling incremental SMT-solving. We demonstrate through a collection of existing benchmarks that the Hybrid-Search algorithm can achieve a 10 times performance improvement in verification times.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_32","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"560-576","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Incremental Rewriting Modulo SMT"],"prefix":"10.1007","author":[{"given":"Gerald","family":"Whitters","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vivek","family":"Nigam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"32_CR1","unstructured":"Anghel, A., Ioannou, N., Parnell, T., Papandreou, N., Mendler-D\u00fcnner, C.: Breadth-first, depth-next training of random forests. In Neural Information Processing Systems (NeurIPS) (2019)"},{"key":"32_CR2","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.scico.2019.03.006","volume":"178","author":"K Bae","year":"2019","unstructured":"Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program. 178, 20\u201342 (2019)","journal-title":"Sci. Comput. Program."},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. In: Formal Aspects of Component Software (FACS) (2019)","DOI":"10.1016\/j.scico.2019.03.006"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Caccamo, M., Buttazzo, G.C., Sha, L.: Capacity sharing for overrun control. In: Proceedings of the 21st IEEE Real-Time Systems Symposium (RTSS 2000), pp. 295\u2013304. IEEE Computer Society (2000)","DOI":"10.1109\/REAL.2000.896018"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Chen, Y., Yang, B., Bryant, R.: Breadth-First with Depth-first BDD Construction: A Hybrid Approach (1997)","DOI":"10.21236\/ADA324567"},{"key":"32_CR6","volume-title":"All About Maude: A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude: A High-Performance Logical Framework, vol. 4350. Springer, Heidelberg (2007)"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Dantas, Y.G., Nigam, V., Fonseca, I.E.: A selective defense for application layer DDoS attacks. In: IEEE Joint Intelligence and Security Informatics Conference, JISIC 2014, pp. 75\u201382. IEEE (2014)","DOI":"10.1109\/JISIC.2014.21"},{"key":"32_CR8","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 de Moura","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":"32_CR9","doi-asserted-by":"crossref","unstructured":"Korf, R.: Depth-First Iterative-Deepening: An Optimal Admissible Tree Search (1985)","DOI":"10.1016\/0004-3702(85)90084-0"},{"key":"32_CR10","series-title":"pp","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-319-13338-6_21","volume-title":"Hardware and Software: Verification and Testing","author":"T Liu","year":"2014","unstructured":"Liu, T., Ara\u00fajo, M., d\u2019Amorim, M., Taghdiri, M.: A comparative study of incremental constraint solving approaches in symbolic execution. In: Yahav, E. (ed.) Hardware and Software: Verification and Testing. pp, pp. 284\u2013299. Springer International Publishing, Cham (2014)"},{"key":"32_CR11","unstructured":"MaudeSE (2021). https:\/\/github.com\/maude-se\/maude-se.github.io"},{"issue":"1","key":"32_CR12","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"32_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-031-12441-9_11","volume-title":"Rewriting Logic and its Applications","author":"V Nigam","year":"2022","unstructured":"Nigam, V., Talcott, C.: Automating safety proofs about cyber-physical systems using rewriting modulo SMT. In: Bae, K. (ed.) WRLA 2022. LNCS, vol. 13252, pp. 212\u2013229. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-12441-9_11"},{"key":"32_CR14","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. J. Logical Algebraic Methods Program. 86, 269\u2013297 (2017)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"32_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-031-12441-9_14","volume-title":"Rewriting Logic and its Applications","author":"R Rubio","year":"2022","unstructured":"Rubio, R.: Maude as a library: an efficient all-purpose programming interface. In: Bae, K. (ed.) WRLA 2022. LNCS, vol. 13252, pp. 274\u2013294. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-12441-9_14"},{"issue":"3","key":"32_CR16","doi-asserted-by":"publisher","first-page":"299","DOI":"10.3233\/JCS-200012","volume":"29","author":"AA Urquiza","year":"2021","unstructured":"Urquiza, A.A., et al.: Resource and timing aspects of security protocols. J. Comput. Secur. 29(3), 299\u2013340 (2021)","journal-title":"J. Comput. Secur."},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Whitters, G., Nigam, V., Talcott, C.: Incremental rewriting modulo SMT experiments (2023). https:\/\/github.com\/WhittersGerald\/cade-incremental-rewriting","DOI":"10.1007\/978-3-031-38499-8_32"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T10:35:40Z","timestamp":1730025340000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","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":"77","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":"28","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":"5","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":"36% - 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":"6","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)"}}]}}