- -

Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME system

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME system

Mostrar el registro completo del ítem

Alpuente Frasnedo, M.; Ballis, D.; Sapiña-Sanchis, J. (2020). Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME system. Mathematics in Computer Science. 14(3):591-606. https://doi.org/10.1007/s11786-020-00455-3

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

Ficheros en el ítem

Thumbnail
Nombre: AlpuenteBallisSap ...
Tamaño: 1.125Mb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: MICS2020-editor.pdf
Tamaño: 2.570Mb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME system
Autor: Alpuente Frasnedo, María Ballis, D. Sapiña-Sanchis, Julia
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] Program specialization is mainly recognized as a powerful technique for optimizing software systems. Nonetheless, it can also be productively employed in other application areas. This paper presents an assertion-guided ...[+]
Palabras clave: Safety properties , Assertions , Program transformation , Maude
Derechos de uso: Reserva de todos los derechos
Fuente:
Mathematics in Computer Science. (issn: 1661-8270 )
DOI: 10.1007/s11786-020-00455-3
Editorial:
Springer
Versión del editor: https://doi.org/10.1007/s11786-020-00455-3
Código del Proyecto:
info:eu-repo/grantAgreement/GVA//APOSTD%2F2019%2F127/
info:eu-repo/grantAgreement/GVA//PROMETEO%2F2019%2F098/ES/DeepTrust: Deep Logic Technology for Software Trustworthiness/
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/
Agradecimientos:
This work has been partially supported by the EU (FEDER) and the Spanish Ministry of Science, Innovation and Universities under grant RTI2018-094403-B-C32, and by Generalitat Valenciana ref. PROMETEO/2019/098 and ref. ...[+]
Tipo: Artículo

References

Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Using conditional trace slicing for improving maude programs. Sci. Comput. Program. 80(Part B), 385–415 (2014)

Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Slicing-based trace analysis of rewriting logic specifications with iJulienne. In: Proceedings of the 22nd European Symposium on Programming (ESOP 2013). LNCS, vol. 7792, pp. 121–124. Springer (2013)

Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Assertion-based analysis via slicing with ABETS. Theory Pract. Log. Program. 16(5–6), 515–532 (2016) [+]
Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Using conditional trace slicing for improving maude programs. Sci. Comput. Program. 80(Part B), 385–415 (2014)

Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Slicing-based trace analysis of rewriting logic specifications with iJulienne. In: Proceedings of the 22nd European Symposium on Programming (ESOP 2013). LNCS, vol. 7792, pp. 121–124. Springer (2013)

Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Assertion-based analysis via slicing with ABETS. Theory Pract. Log. Program. 16(5–6), 515–532 (2016)

Alpuente, M., Ballis, D., Sapiña, J.: Inferring safe Maude programs with ÁTAME. In: Mathematical Software—ICMS 2018—6th International Conference. LNCS, vol. 10931, pp. 1–10. Springer (2018)

Alpuente, M., Ballis, D., Sapiña, J.: Imposing assertions in Maude via program transformation. MethodsX 6, 2577–2583 (2019)

Alpuente, M., Ballis, D., Sapiña, J.: Static correction of Maude programs with assertions. J. Syst. Softw. 153, 64–85 (2019)

Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: Partial evaluation of order-sorted equational programs modulo axioms. In: Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016). LNCS, vol. 10184, pp. 3–20. Springer (2016)

Clavel, M., Durán, F., Eker, S., Escobar, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude manual (version 3.0). Technical report, SRI International Computer Science Laboratory (2019). http://maude.lcc.uma.es/maude30-manual-html/maude-manual.html. Accessed 24 Jan 2020

Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Proceedings of POPL 2000, pp. 54–66. ACM (2000)

Danvy, O., Glück, R., Thiemann, P. (eds.): Proceedings of the International Seminar on Partial Evaluation (Dagstuhl 1996). LNCS, vol. 1110. Springer (1996)

Joiner, R., Reps, T., Jha, S., Dhawan, M., Ganapathy, V.: Efficient runtime-enforcement techniques for policy weaving. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2014), pp. 224–234. ACM (2014)

Khoo, S.C., Shi, K.: Program adaptation via output-constraint specialization. High. Order Symb. Comput. 17(1), 93–128 (2004)

Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)

Puebla, G., Bueno, F., Hermenegildo, M.V.: Combined static and dynamic assertion-based debugging of constraint logic programs. In: Proceedings of the 9th International Workshop on Logic Programming Synthesis and Transformation (LOPSTR 1999), Selected Papers. LNCS, vol. 1817, pp. 273–292. Springer (2000)

The Anima Website (2015). http://safe-tools.dsic.upv.es/anima. Accessed 24 Jan 2020

Vazou, N., Seidel, E.L., Jhala, R.: LiquidHaskell: experience with refinement types in the real world. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, pp. 39–51 (2014)

[-]

recommendations

 

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

Mostrar el registro completo del ítem