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 |