{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T05:22:38Z","timestamp":1771910558762,"version":"3.50.1"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319680330","type":"print"},{"value":"9783319680347","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68034-7_5","type":"book-chapter","created":{"date-parts":[[2017,9,13]],"date-time":"2017-09-13T17:32:45Z","timestamp":1505323965000},"page":"78-97","source":"Crossref","is-referenced-by-count":10,"title":["Guarded Terms for Rewriting Modulo SMT"],"prefix":"10.1007","author":[{"given":"Kyungmin","family":"Bae","sequence":"first","affiliation":[]},{"given":"Camilo","family":"Rocha","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,14]]},"reference":[{"issue":"1","key":"5_CR1","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. Softw. Tools Technol. Transf. 11(1), 69\u201383 (2009)","journal-title":"Softw. Tools Technol. Transf."},{"key":"5_CR2","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: RTA. LIPIcs, vol. 21, pp. 81\u201396. Schloss Dagstuhl (2013)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-319-06410-9_7","volume-title":"FM 2014: Formal Methods","author":"K Bae","year":"2014","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of Multirate Synchronous AADL. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 94\u2013109. Springer, Cham (2014). doi: 10.1007\/978-3-319-06410-9_7"},{"issue":"12","key":"5_CR4","doi-asserted-by":"crossref","first-page":"1235","DOI":"10.1016\/j.scico.2010.10.002","volume":"77","author":"K Bae","year":"2012","unstructured":"Bae, K., \u00d6lveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. Sci. Comput. Program. 77(12), 1235\u20131271 (2012)","journal-title":"Sci. Comput. Program."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bae, K., Rocha, C.: A Note on Guarded Terms for Rewriting Modulo SMT, July 2017. http:\/\/sevlab.postech.ac.kr\/~kmbae\/rew-smt","DOI":"10.1007\/978-3-319-68034-7_5"},{"issue":"1\u20133","key":"5_CR6","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoret. Comput. Sci. 360(1\u20133), 386\u2013414 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Caccamo, M., Buttazzo, G., Sha, L.: Capacity sharing for overrun control. In: RTSS, pp. 295\u2013304. IEEE (2000)","DOI":"10.1109\/REAL.2000.896018"},{"key":"5_CR8","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224 (2008)"},{"issue":"2","key":"5_CR9","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277\u2013293. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_23"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"77","DOI":"10.4204\/EPTCS.18.6","volume":"18","author":"G Dowek","year":"2010","unstructured":"Dowek, G., Mu\u00f1oz, C., Rocha, C.: Rewriting logic semantics of a plan execution language. Electron. Proc. Theor. Comput. Sci. 18, 77\u201391 (2010)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S., Lahiri, S.: Corral: a solver for reachability modulo theories. Technical report MSR-TR-2012-9, Microsoft Research, January 2012","DOI":"10.1007\/978-3-642-31424-7_32"},{"issue":"1","key":"5_CR14","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"7\u20138","key":"5_CR15","doi-asserted-by":"crossref","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81(7\u20138), 721\u2013781 (2012)","journal-title":"J. Logic Algebraic Program."},{"issue":"1\u20132","key":"5_CR16","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. High.-Ord. Symbolic Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"High.-Ord. Symbolic Comput."},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11693017_26","volume-title":"Fundamental Approaches to Software Engineering","author":"PC \u00d6lveczky","year":"2006","unstructured":"\u00d6lveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 357\u2013372. Springer, Heidelberg (2006). doi: 10.1007\/11693017_26"},{"key":"5_CR18","unstructured":"Rocha, C.: Symbolic Reachability Analysis for Rewrite Theories. Ph.D. thesis, University of Illinois, December 2012"},{"issue":"1","key":"5_CR19","doi-asserted-by":"crossref","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. Log. Algebraic Methods Program. 86(1), 269\u2013297 (2017)","journal-title":"J. Log. Algebraic Methods Program."}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68034-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T12:36:56Z","timestamp":1570106216000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68034-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319680330","9783319680347"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68034-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}