- -

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Mostrar el registro completo del ítem

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

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/124698

Ficheros en el ítem

Thumbnail
Nombre: Gutiérrez;Meseguer ...
Tamaño: 461.6Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: lopstr17.pdf
Tamaño: 395.9Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Variant-Based Decidable Satisfiability in Initial Algebras with Predicates
Autor: Gutiérrez Gil, Raúl Meseguer, José
Entidad UPV: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Fecha difusión:
Resumen:
[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 ...[+]
Palabras clave: Finite variant property (fvp) , OS-compactness , User-definable predicates , Decidable validity and satisfiability in initial algebras
Derechos de uso: Reserva de todos los derechos
Fuente:
Lecture Notes in Computer Science. (issn: 0302-9743 )
DOI: 10.1007/978-3-319-94460-9_18
Editorial:
Springer-Verlag
Versión del editor: https://doi.org/10.1007/978-3-319-94460-9_18
Título del congreso: 27th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2017)
Lugar del congreso: Namur, Blegium
Fecha congreso: Octubre 10-12,2017
Código del Proyecto:
info:eu-repo/grantAgreement/MINECO//TIN2015-69175-C4-1-R/ES/SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA/
info:eu-repo/grantAgreement/NSF//1409416/US/CSR: Medium: Availability-Consistency Tradeoffs in Key-Value and NoSQL Storage Systems/
info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/
info:eu-repo/grantAgreement/INCIBE//INCIBEI-2015-27346/
info:eu-repo/grantAgreement/NRL//N00173-17-1-G002/
Agradecimientos:
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 ...[+]
Tipo: Artículo Comunicación en congreso

References

Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. TOCL 10(1), 4 (2009)

Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. I&C 183(2), 140–164 (2003)

Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. JSAT 3, 21–46 (2007) [+]
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. TOCL 10(1), 4 (2009)

Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. I&C 183(2), 140–164 (2003)

Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. JSAT 3, 21–46 (2007)

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

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

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

Ciobaca., S.: Verification of composition of security protocols with applications to electronic voting. Ph.D. thesis, ENS Cachan (2011)

Comon, H.: Complete axiomatizations of some quotient term algebras. TCS 118(2), 167–191 (1993)

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

Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Handbook of Theoretical Computer Science, North-Holland, vol. B, pp. 243–320 (1990)

Dovier, A., Piazza, C., Rossi, G.: A uniform approach to constraint-solving for lists, multisets, compact lists, and sets. TOCL 9(3), 15 (2008)

Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Adding decision procedures to SMT solvers using axioms with triggers. JAR 56(4), 387–457 (2016)

Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. JALP 81, 898–928 (2012)

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

Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. TCS 105, 217–273 (1992)

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

Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SICOMP 15, 1155–1194 (1986)

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

Lynch, C., Morawska, B.: Automatic decidability. In: Proceedings of LICS 2002, p. 7. IEEE Computer Society (2002)

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

Meseguer, J.: Variant-based satisfiability in initial algebras. SCP 154, 3–41 (2018)

Meseguer, J.: Strict coherence of conditional rewriting modulo axioms. TCS 672, 1–35 (2017)

Meseguer, J., Goguen, J.: Initiality, induction and computability. In: Algebraic Methods in Semantics, Cambridge, pp. 459–541 (1985)

Meseguer, J., Goguen, J.: Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. I&C 103(1), 114–158 (1993)

Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS 1(2), 245–257 (1979)

Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1–12 (1984)

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

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)

Tushkanova, E., Giorgetti, A., Ringeissen, C., Kouchnarenko, O.: A rule-based system for automatic decidability and combinability. SCP 99, 3–23 (2015)

[-]

recommendations

 

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

Mostrar el registro completo del ítem