- -

Automatically Proving and Disproving Feasibility Conditions

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Automatically Proving and Disproving Feasibility Conditions

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: GutierrezLucas - ...
Tamaño: 577.9Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: GutLuc_Automatica ...
Tamaño: 605.4Kb
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:12Z
dc.date.available 2021-12-21T06:57:12Z
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/178662
dc.description.abstract [EN] In the realm of term rewriting, given terms s and t, a reachability condition s>>t is called feasible if there is a substitution O such that O(s) rewrites into O(t) in zero or more steps; otherwise, it is called infeasible. Checking infeasibility of (sequences of) reachability conditions is important in the analysis of computational properties of rewrite systems like confluence or (operational) termination. In this paper, we generalize this notion of feasibility to arbitrary n-ary relations on terms defined by first-order theories. In this way, properties of computational systems whose operational semantics can be given as a first-order theory can be investigated. We introduce a framework for proving feasibility/infeasibility, and a new tool, infChecker, which implements it. 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 Conditional rewriting es_ES
dc.subject Feasibility es_ES
dc.subject Program analysis es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Automatically Proving and Disproving Feasibility Conditions 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_27 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///PROMETEO%2F2019%2F098//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). Automatically Proving and Disproving Feasibility Conditions. Springer Nature. 416-435. https://doi.org/10.1007/978-3-030-51054-1_27 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_27 es_ES
dc.description.upvformatpinicio 416 es_ES
dc.description.upvformatpfin 435 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.relation.pasarela S\428792 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.description.references Andrianarivelo, N., Réty, P.: Over-approximating terms reachable by context-sensitive rewriting. In: Bojańczyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 128–139. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24537-9_12 es_ES
dc.description.references Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3(1/2), 69–116 (1987). https://doi.org/10.1016/S0747-7171(87)80022-6 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.: Models and equality for logical programming. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol. 250, pp. 1–22. Springer, Heidelberg (1987). https://doi.org/10.1007/BFb0014969 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 Kojima, Y., Sakai, M.: Innermost reachability and context sensitive reachability properties are decidable for linear right-shallow term rewriting systems. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 187–201. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70590-1_13 es_ES
dc.description.references Kojima, Y., Sakai, M., Nishida, N., Kusakari, K., Sakabe, T.: Context-sensitive innermost reachability is decidable for linear right-shallow term rewriting systems. Inf. Media Technol. 4(4), 802–814 (2009) es_ES
dc.description.references Kojima, Y., Sakai, M., Nishida, N., Kusakari, K., Sakabe, T.: Decidability of reachability for right-shallow context-sensitive term rewriting systems. IPSJ Online Trans. 4, 192–216 (2011) es_ES
dc.description.references Lucas, S.: Analysis of rewriting-based systems as first-order theories. In: Fioravanti, F., Gallagher, J.P. (eds.) LOPSTR 2017. LNCS, vol. 10855, pp. 180–197. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94460-9_11 es_ES
dc.description.references Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Funct. Logic Program. 1998(1) (1998). http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1998/A98-01/A98-01.html 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.: Using well-founded relations for proving operational termination. J. Autom. Reasoning 64(2), 167–195 (2019). https://doi.org/10.1007/s10817-019-09514-2 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.: Proving operational termination of declarative programs in general logics. In: Chitil, O., King, A., Danvy, O. (eds.) Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, 8–10 September 2014, pp. 111–122. ACM (2014). https://doi.org/10.1145/2643135.2643152 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, in press) es_ES
dc.description.references McCune, W.: Prover9 and Mace4. https://www.cs.unm.edu/~mccune/mace4/ es_ES
dc.description.references Meßner, F., Sternagel, C.: nonreach – a tool for nonreachability analysis. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 337–343. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_19 es_ES
dc.description.references Middeldorp, A., Nagele, J., Shintani, K.: Confluence competition 2019. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 25–40. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_2 es_ES
dc.description.references Nishida, N., Maeda, Y.: Narrowing trees for syntactically deterministic conditional term rewriting systems. In: Kirchner, H. (ed.) Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction. FSCD 2018. Leibniz International Proceedings in Informatics (LIPIcs), vol. 108, pp. 26:1–26:20. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018). https://doi.org/10.4230/LIPIcs.FSCD.2018.26 es_ES
dc.description.references Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002). http://www.springer.com/computer/swe/book/978-0-387-95250-5 es_ES
dc.description.references Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Dover, New York (2006) es_ES
dc.description.references Sternagel, C., Sternagel, T., Middeldorp, A.: CoCo 2018 Participant: ConCon 1.5. In: Felgenhauer, B., Simonsen, J. (eds.) Proceedings of the 7th International Workshop on Confluence. IWC 2018, p. 66 (2018). http://cl-informatik.uibk.ac.at/events/iwc-2018/ es_ES
dc.description.references Sternagel, C., Yamada, A.: Reachability analysis for termination and confluence of rewriting. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 262–278. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_15 es_ES
dc.description.references Winkler, S., Moser, G.: MædMax: a maximal ordered completion tool. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 472–480. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_31 es_ES


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

Mostrar el registro sencillo del ítem