- -

MU-TERM: Verify Termination Properties Automatically (System Description)

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

MU-TERM: Verify Termination Properties Automatically (System Description)

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: GutierrezLucas - ...
Tamaño: 469.5Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: LucGut_MuTermVeri ...
Tamaño: 395.3Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Gutiérrez Gil, Raúl es_ES
dc.contributor.author Lucas Alba, Salvador es_ES
dc.date.accessioned 2021-12-21T06:57:14Z
dc.date.available 2021-12-21T06:57:14Z
dc.date.issued 2020-07-06 es_ES
dc.identifier.isbn 978-3-030-51053-4 es_ES
dc.identifier.issn 0302-9743 es_ES
dc.identifier.uri http://hdl.handle.net/10251/178664
dc.description.abstract [EN] We report on the new version of mu-term, a tool for proving termination properties of variants of rewrite systems, including conditional, context-sensitive, equational, and order-sorted rewrite systems. We follow a unified logic-based approach to describe rewriting computations. The automatic generation of logical models for suitable first-order theories and formulas provide a common basis to implement the proofs. es_ES
dc.description.sponsorship Supported by EU (FEDER), and projects RTI2018-094403-B-C32,PROMETEO/ 2019/098, and SP20180225. Also by INCIBE program "Ayudas para la excelencia de los equipos de investigación avanzada en ciberseguridad" (Raul Gutiérrez). es_ES
dc.language Inglés es_ES
dc.publisher Springer Nature es_ES
dc.relation.ispartof Automated Reasoning. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II es_ES
dc.relation.ispartofseries Lecture Notes in Computer Science;12167 es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Program analysis es_ES
dc.subject Term Rewriting es_ES
dc.subject Termination es_ES
dc.subject Tools es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title MU-TERM: Verify Termination Properties Automatically (System Description) es_ES
dc.type Comunicación en congreso es_ES
dc.type Artículo es_ES
dc.type Capítulo de libro es_ES
dc.identifier.doi 10.1007/978-3-030-51054-1_28 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/UPV//SP20180225/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEO%2F2019%2F098/ES/DEEPTRUST/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Gutiérrez Gil, R.; Lucas Alba, S. (2020). MU-TERM: Verify Termination Properties Automatically (System Description). Springer Nature. 436-447. https://doi.org/10.1007/978-3-030-51054-1_28 es_ES
dc.description.accrualMethod S es_ES
dc.relation.conferencename 10th International Joint Conference on Automated Reasoning (IJCAR 2020) es_ES
dc.relation.conferencedate Junio 29-Julio 06,2020 es_ES
dc.relation.conferenceplace Paris, France es_ES
dc.relation.publisherversion https://doi.org/10.1007/978-3-030-51054-1_28 es_ES
dc.description.upvformatpinicio 436 es_ES
dc.description.upvformatpfin 447 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.relation.pasarela S\428795 es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.contributor.funder Instituto Nacional de Ciberseguridad es_ES
dc.contributor.funder Universitat Politècnica de València es_ES
dc.contributor.funder Generalitat Valenciana
dc.description.references Alarcón, B., et al.: Improving context-sensitive dependency pairs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 636–651. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89439-1_44 es_ES
dc.description.references Alarcón, B., Gutiérrez, R., Lucas, S.: Context-sensitive dependency pairs. Inf. Comput. 208(8), 922–968 (2010). https://doi.org/10.1016/j.ic.2010.03.003 es_ES
dc.description.references Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201–208. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-17796-5_12 es_ES
dc.description.references Alarcón, B., Lucas, S., Meseguer, J.: A dependency pair framework for $${A} \vee {C}$$-termination. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 35–51. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16310-4_4 es_ES
dc.description.references Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8 es_ES
dc.description.references Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1 es_ES
dc.description.references Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reasoning 40(2–3), 195–220 (2008). https://doi.org/10.1007/s10817-007-9087-9 es_ES
dc.description.references Giesl, J., Arts, T.: Verification of erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12(1/2), 39–72 (2001). https://doi.org/10.1007/s002000100063 es_ES
dc.description.references Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_12 es_ES
dc.description.references Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reasoning 37(3), 155–203 (2006). https://doi.org/10.1007/s10817-006-9057-7 es_ES
dc.description.references Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217–273 (1992). https://doi.org/10.1016/0304-3975(92)90302-V es_ES
dc.description.references Gutiérrez, R., Lucas, S.: Function calls at frozen positions in termination of context-sensitive rewriting. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 311–330. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23165-5_15 es_ES
dc.description.references Gutiérrez, R., Lucas, S.: Proving termination in the context-sensitive dependency pair framework. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 18–34. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16310-4_3 es_ES
dc.description.references Gutiérrez, R., Lucas, S.: Automatic generation of logical models with AGES. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 287–299. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29436-6_17 es_ES
dc.description.references Gutiérrez, R., Lucas, S.: Automatically proving and disproving feasibility conditions. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNAI, vol. 12167, pp. 416–435. Springer, Heidelberg (2020) es_ES
dc.description.references Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Funct. Log. Program. 1998(1), 1–61 (1998). http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1998/A98-01/A98-01.html es_ES
dc.description.references Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294–343 (2002). https://doi.org/10.1006/inco.2002.3176 es_ES
dc.description.references Lucas, S.: Proving semantic properties as first-order satisfiability. Artif. Intell. 277 (2019). https://doi.org/10.1016/j.artint.2019.103174 es_ES
dc.description.references Lucas, S., Gutiérrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reasoning 60(4), 465–501 (2017). https://doi.org/10.1007/s10817-017-9419-3 es_ES
dc.description.references Lucas, S., Gutiérrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90–95 (2018). https://doi.org/10.1016/j.ipl.2018.04.002 es_ES
dc.description.references Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95(4), 446–453 (2005). https://doi.org/10.1016/j.ipl.2005.05.002 es_ES
dc.description.references Lucas, S., Meseguer, J.: Order-sorted dependency pairs. In: Antoy, S., Albert, E. (eds.) Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 15–17 July 2008, Valencia, Spain, pp. 108–119. ACM (2008). https://doi.org/10.1145/1389449.1389463 es_ES
dc.description.references Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebraic Methods Program. 86(1), 236–268 (2017). https://doi.org/10.1016/j.jlamp.2016.03.003 es_ES
dc.description.references Lucas, S., Meseguer, J., Gutiérrez, R.: The 2D dependency pair framework for conditional rewrite systems. Part I: Definition and basic processors. J. Comput. Syst. Sci. 96, 74–106 (2018). https://doi.org/10.1016/j.jcss.2018.04.002 es_ES
dc.description.references Lucas, S., Meseguer, J., Gutiérrez, R.: The 2D dependency pair framework for conditional rewrite systems—part II: advanced processors and implementation techniques. J. Autom. Reasoning (2020). https://doi.org/10.1007/s10817-020-09542-3 es_ES
dc.description.references McCune, W.: Prover9 & Mace4. Technical report (2005–2010). http://www.cs.unm.edu/~mccune/prover9/ es_ES
dc.description.references Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer (2002). https://doi.org/10.1007/978-1-4757-3661-8 . http://www.springer.com/computer/swe/book/978-0-387-95250-5 es_ES
dc.description.references Ölveczky, P.C., Lysne, O.: Order-sorted termination: the unsorted way. In: Hanus, M., Rodríguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol. 1139, pp. 92–106. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61735-3_6 es_ES
dc.description.references Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17(1), 23–50 (1994). https://doi.org/10.1006/jsco.1994.1003 es_ES
dc.description.references Zantema, H.: Termination of context-sensitive rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 172–186. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-62950-5_69 es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem