Mostrar el registro sencillo del ítem
dc.contributor.author | Gutiérrez Gil, Raúl | es_ES |
dc.contributor.author | Meseguer, José | es_ES |
dc.date.accessioned | 2019-08-02T20:00:52Z | |
dc.date.available | 2019-08-02T20:00:52Z | |
dc.date.issued | 2018 | es_ES |
dc.identifier.issn | 0302-9743 | es_ES |
dc.identifier.uri | http://hdl.handle.net/10251/124698 | |
dc.description.abstract | [EN] Decision procedures can be either theory-specific, e.g., Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure for quantifier-free satisfiability in the initial algebra of an order-sorted equational theory (¿,E¿B) under two conditions: (i) E¿B has the finite variant property and B has a finitary unification algorithm; and (ii) (¿,E¿B) protects a constructor subtheory (¿,E¿¿B¿) that is OS-compact. These conditions apply to many user-definable theories, but have a main limitation: they apply well to data structures, but often do not hold for user-definable predicates on such data structures. We present a theory-generic satisfiability decision procedure, and a prototype implementation, extending variant-based satisfiability to initial algebras with user-definable predicates under fairly general conditions. | es_ES |
dc.description.sponsorship | Partially supported by NSF Grant CNS 14-09416, NRL under contract number N00173-17-1-G002, the EU (FEDER), Spanish MINECO project TIN2015-69175- C4-1-R and GV project PROMETEOII/2015/013. Ra´ul Guti´errez was also supported by INCIBE program “Ayudas para la excelencia de los equipos de investigaci´on avanzada en ciberseguridad”. | |
dc.language | Inglés | es_ES |
dc.publisher | Springer-Verlag | es_ES |
dc.relation.ispartof | Lecture Notes in Computer Science | es_ES |
dc.rights | Reserva de todos los derechos | es_ES |
dc.subject | Finite variant property (fvp) | es_ES |
dc.subject | OS-compactness | es_ES |
dc.subject | User-definable predicates | es_ES |
dc.subject | Decidable validity and satisfiability in initial algebras | es_ES |
dc.subject.classification | LENGUAJES Y SISTEMAS INFORMATICOS | es_ES |
dc.title | Variant-Based Decidable Satisfiability in Initial Algebras with Predicates | es_ES |
dc.type | Artículo | es_ES |
dc.type | Comunicación en congreso | es_ES |
dc.identifier.doi | 10.1007/978-3-319-94460-9_18 | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/MINECO//TIN2015-69175-C4-1-R/ES/SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/NSF//1409416/US/CSR: Medium: Availability-Consistency Tradeoffs in Key-Value and NoSQL Storage Systems/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/INCIBE//INCIBEI-2015-27346/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/NRL//N00173-17-1-G002/ | |
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.; Meseguer, J. (2018). Variant-Based Decidable Satisfiability in Initial Algebras with Predicates. Lecture Notes in Computer Science. 10855:306-322. https://doi.org/10.1007/978-3-319-94460-9_18 | es_ES |
dc.description.accrualMethod | S | es_ES |
dc.relation.conferencename | 27th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2017) | es_ES |
dc.relation.conferencedate | Octubre 10-12,2017 | es_ES |
dc.relation.conferenceplace | Namur, Blegium | es_ES |
dc.relation.publisherversion | https://doi.org/10.1007/978-3-319-94460-9_18 | es_ES |
dc.description.upvformatpinicio | 306 | es_ES |
dc.description.upvformatpfin | 322 | es_ES |
dc.type.version | info:eu-repo/semantics/publishedVersion | es_ES |
dc.description.volume | 10855 | es_ES |
dc.relation.pasarela | S\376345 | es_ES |
dc.contributor.funder | Generalitat Valenciana | es_ES |
dc.contributor.funder | Ministerio de Economía y Empresa | es_ES |
dc.contributor.funder | Instituto Nacional de Ciberseguridad | es_ES |
dc.contributor.funder | National Science Foundation, EEUU | |
dc.contributor.funder | U.S. Naval Research Laboratory | |
dc.description.references | Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. TOCL 10(1), 4 (2009) | es_ES |
dc.description.references | Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. I&C 183(2), 140–164 (2003) | es_ES |
dc.description.references | Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. JSAT 3, 21–46 (2007) | es_ES |
dc.description.references | Bouchard, C., Gero, K.A., Lynch, C., Narendran, P.: On forward closure and the finite variant property. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 327–342. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40885-4_23 | es_ES |
dc.description.references | Bradley, A.R., Manna, Z.: The Calculus of Computation - Decision Procedures with Applications to Verification. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74113-8 | es_ES |
dc.description.references | Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, CS Dept. University of Illinois at Urbana-Champaign (2014). http://hdl.handle.net/2142/47117 | es_ES |
dc.description.references | Ciobaca., S.: Verification of composition of security protocols with applications to electronic voting. Ph.D. thesis, ENS Cachan (2011) | es_ES |
dc.description.references | Comon, H.: Complete axiomatizations of some quotient term algebras. TCS 118(2), 167–191 (1993) | es_ES |
dc.description.references | Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32033-3_22 | es_ES |
dc.description.references | Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Handbook of Theoretical Computer Science, North-Holland, vol. B, pp. 243–320 (1990) | es_ES |
dc.description.references | Dovier, A., Piazza, C., Rossi, G.: A uniform approach to constraint-solving for lists, multisets, compact lists, and sets. TOCL 9(3), 15 (2008) | es_ES |
dc.description.references | Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Adding decision procedures to SMT solvers using axioms with triggers. JAR 56(4), 387–457 (2016) | es_ES |
dc.description.references | Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. JALP 81, 898–928 (2012) | 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 | Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. TCS 105, 217–273 (1992) | es_ES |
dc.description.references | Gutiérrez, R., Meseguer, J.: Variant satisfiability in initial algebras with predicates. Technical report, CS Department, University of Illinois at Urbana-Champaign (2018). http://hdl.handle.net/2142/99039 | es_ES |
dc.description.references | Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SICOMP 15, 1155–1194 (1986) | es_ES |
dc.description.references | Kroening, D., Strichman, O.: Decision Procedures - An algorithmic point of view. Texts in TCS. An EATCS Series. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-74105-3 | es_ES |
dc.description.references | Lynch, C., Morawska, B.: Automatic decidability. In: Proceedings of LICS 2002, p. 7. IEEE Computer Society (2002) | es_ES |
dc.description.references | Lynch, C., Tran, D.-K.: Automatic decidability and combinability revisited. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 328–344. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_22 | es_ES |
dc.description.references | Meseguer, J.: Variant-based satisfiability in initial algebras. SCP 154, 3–41 (2018) | es_ES |
dc.description.references | Meseguer, J.: Strict coherence of conditional rewriting modulo axioms. TCS 672, 1–35 (2017) | es_ES |
dc.description.references | Meseguer, J., Goguen, J.: Initiality, induction and computability. In: Algebraic Methods in Semantics, Cambridge, pp. 459–541 (1985) | es_ES |
dc.description.references | Meseguer, J., Goguen, J.: Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. I&C 103(1), 114–158 (1993) | es_ES |
dc.description.references | Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS 1(2), 245–257 (1979) | es_ES |
dc.description.references | Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1–12 (1984) | es_ES |
dc.description.references | Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. In: Lucanu, D. (ed.) WRLA 2016. LNCS, vol. 9942, pp. 167–184. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-44802-2_10 | es_ES |
dc.description.references | Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: Proceedings of LICS 2001, pp. 29–37. IEEE (2001) | es_ES |
dc.description.references | Tushkanova, E., Giorgetti, A., Ringeissen, C., Kouchnarenko, O.: A rule-based system for automatic decidability and combinability. SCP 99, 3–23 (2015) | es_ES |