- -

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

  • Estadisticas de Uso

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Show simple item record

Files in this item

Thumbnail
Name: Gutiérrez;Meseguer ...
Size: 461.6Kb
Format: PDF
Description: Versión del Autor.
Open
[Cerrado]
Name: lopstr17.pdf
Size: 395.9Kb
Format: PDF
Description: Versión editorial
Request a copy of the document
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


This item appears in the following Collection(s)

Show simple item record