{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:26:01Z","timestamp":1725863161845},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319448015"},{"type":"electronic","value":"9783319448022"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-44802-2_8","type":"book-chapter","created":{"date-parts":[[2016,8,17]],"date-time":"2016-08-17T12:32:52Z","timestamp":1471437172000},"page":"134-151","source":"Crossref","is-referenced-by-count":2,"title":["Proving Reachability-Logic Formulas Incrementally"],"prefix":"10.1007","author":[{"given":"Vlad","family":"Rusu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Arusoaie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,18]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/978-3-642-31585-5_33","volume-title":"Automata, Languages, and Programming","author":"G Ro\u015fu","year":"2012","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Towards a unified theory of operational and axiomatic semantics. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 351\u2013363. Springer, Heidelberg (2012)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Checking reachability using matching logic. In: Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012), pp. 555\u2013574. ACM (2012)","DOI":"10.1145\/2384616.2384656"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A., Ciob\u00e2c\u0103, \u015e., Moore, B.M.: One-path reachability logic. In: Proceedings of the 28th Symposium on Logic in Computer Science (LICS 2013), pp. 358\u2013367. IEEE, June 2013","DOI":"10.1109\/LICS.2013.42"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-319-08918-8_29","volume-title":"Rewriting and Typed Lambda Calculi","author":"A \u015etef\u0103nescu","year":"2014","unstructured":"\u015etef\u0103nescu, A., Ciob\u00e2c\u0103, \u015e., Mereu\u0163\u0103, R., Moore, B.M., \u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 425\u2013440. Springer, Heidelberg (2014)"},{"key":"8_CR5","unstructured":"Arusoaie, A., Lucanu, D., Rusu, V.: A generic framework for symbolic execution: theory and applications. Research report RR-8189. Inria, September 2015"},{"key":"8_CR6","unstructured":"Arusoaie, A., Lucanu, D., Rusu, V.: A generic framework for symbolic execution. Research report RR-8189. Inria, September 2015. https:\/\/hal.inria.fr\/hal-00766220"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-642-17796-5_9","volume-title":"Algebraic Methodology and Software Technology","author":"G Ro\u015fu","year":"2011","unstructured":"Ro\u015fu, G., Ellison, C., Schulte, W.: Matching logic: an alternative to Hoare\/Floyd logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 142\u2013162. Springer, Heidelberg (2011)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Matching logic: a new program verification approach (NIER track). In: ICSE 2011: Proceedings of the 30th International Conference on Software Engineering, pp. 868\u2013871. ACM (2011)","DOI":"10.1145\/1985793.1985928"},{"key":"8_CR11","unstructured":"Ro\u015fu, G.: Matching logic \u2014 extended abstract. In: Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol. 36, pp. 5\u201321. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, July 2015"},{"key":"8_CR12","unstructured":"Verification of the KMP algorithm. https:\/\/fmse.info.uaic.ro\/imgs\/kmp.pdf"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/978-3-319-23165-5_21","volume-title":"Logic, Rewriting, and Concurrency","author":"D Lucanu","year":"2015","unstructured":"Lucanu, D., Rusu, V., Arusoaie, A., Nowak, D.: Verifying reachability-logic properties on rewriting-logic specifications. In: Mart\u00ed-Oliet, N., \u00d6lveczky, P.C., Talcott, C. (eds.) Meseguer Festschrift. LNCS, vol. 9200, pp. 451\u2013474. Springer, Heidelberg (2015)"},{"issue":"2","key":"8_CR14","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"key":"8_CR16","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods","author":"WP Roever de","year":"2001","unstructured":"de Roever, W.P., de Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press, Cambridge (2001)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-44802-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,12]],"date-time":"2019-09-12T13:05:53Z","timestamp":1568293553000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-44802-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319448015","9783319448022"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-44802-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}