- -

Towards Erlang Verification by Term Rewriting

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Towards Erlang Verification by Term Rewriting

Mostrar el registro completo del ítem

Vidal Oriola, GF. (2013). Towards Erlang Verification by Term Rewriting. En Logic-Based Program Synthesis and Transformation. Springer. 109-126. doi:10.1007/978-3-319-14125-1_7

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

Ficheros en el ítem

Thumbnail
Nombre: paper.pdf
Tamaño: 302.0Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: Vidal_Towards Erlang ...
Tamaño: 3.306Mb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Towards Erlang Verification by Term Rewriting
Autor: Vidal Oriola, Germán Francisco
Entidad UPV: Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica
Fecha difusión:
Resumen:
This paper presents a transformational approach to the verification of Erlang programs. We define a stepwise transformation from (first-order) Erlang programs to (non-deterministic) term rewrite systems that compute an ...[+]
Derechos de uso: Reserva de todos los derechos
ISBN: 978-3-319-14124-4
Fuente:
Logic-Based Program Synthesis and Transformation. (issn: 0302-9743 )
DOI: 10.1007/978-3-319-14125-1_7
Editorial:
Springer
Versión del editor: http://link.springer.com/chapter/10.1007/978-3-319-14125-1_7
Título del congreso: 23rd International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2013)
Lugar del congreso: Madrid, Spain
Fecha congreso: September 18-19, 2013
Serie: Lecture Notes in Computer Science;8901
Descripción: The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-14125-1_7
Tipo: Capítulo de libro Comunicación en congreso

References

Albert, E., Arenas, P., Gómez-Zamalloa, M.: Symbolic Execution of Concurrent Objects in CLP. In: Russo, C., Zhou, N.-F. (eds.) PADL 2012. LNCS, vol. 7149, pp. 123–137. Springer, Heidelberg (2012)

Albert, E., Vidal, G.: The narrowing-driven approach to functional logic program specialization. New Generation Computing 20(1), 3–26 (2002)

Joe, A., Robert, V., Williams, M.: Concurrent programming in ERLANG. Prentice Hall (1993) [+]
Albert, E., Arenas, P., Gómez-Zamalloa, M.: Symbolic Execution of Concurrent Objects in CLP. In: Russo, C., Zhou, N.-F. (eds.) PADL 2012. LNCS, vol. 7149, pp. 123–137. Springer, Heidelberg (2012)

Albert, E., Vidal, G.: The narrowing-driven approach to functional logic program specialization. New Generation Computing 20(1), 3–26 (2002)

Joe, A., Robert, V., Williams, M.: Concurrent programming in ERLANG. Prentice Hall (1993)

Arts, T., Earle, C.B., Derrick, J.: Development of a verified Erlang program for resource locking. STTT 5(2–3), 205–220 (2004)

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)

Caballero, R., Martin-Martin, E., Riesco, A., Tamarit, S.: A Declarative Debugger for Sequential Erlang Programs. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 96–114. Springer, Heidelberg (2013)

Claessen, K., Svensson, H.: A semantics for distributed Erlang. In: Sagonas, K.F., Armstrong, J. (eds.). In: Proc. of the 2005 ACM SIGPLAN Workshop on Erlang, pp. 78–87. ACM (2005)

Earle, C.B.: Symbolic program execution using the Erlang verification tool. In: Alpuente, M. (eds.) Proc. of the 9th International Workshop on Functional and Logic Programming (WFLP 2000), pp. 42–55 (2000)

Felleisen, M., Friedman, D.P., Kohlbecker, E.E., Duba, B.F.: A syntactic theory of sequential control. Theor. Comput. Sci. 52, 205–237 (1987)

Fredlund, L.-A., Svensson, H.: McErlang: a model checker for a distributed functional programming language. In: Hinze, R., Ramsey, N. (eds). In: Proc. of ICFP 2007, pp. 125–136. ACM (2007)

Giesl, J., Arts, T.: Verification of Erlang Processes by Dependency Pairs. Appl. Algebra Eng. Commun. Comput. 12(1/2), 39–72 (2001)

Hanus, M. (ed.): Curry: An integrated functional logic language (vers. 0.8.3) (2012), http://www.curry-language.org

Huch, F.: Verification of Erlang Programs using Abstract Interpretation and Model Checking. In: Rémi, D., Lee, P. (eds.) Proc. of ICFP 1999, pp. 261–272. ACM (1999)

J.-M., H.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) 5th Conference on Automated Deduction Les Arcs. LNCS, pp. 318–334. Springer, Heidelberg (1980)

Leucker, M., Noll, T.: Rewriting Logic as a Framework for Generic Verification Tools. Electr. Notes Theor. Comput. Sci. 36, 121–137 (2000)

Meseguer, J.: Conditioned Rewriting Logic as a United Model of Concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)

Neuhäußer, M.R., Noll, T.: Abstraction and Model Checking of Core Erlang Programs in Maude. Electr. Notes Theor. Comput. Sci. 176(4), 147–163 (2007)

Nishida, N., Vidal, G.: A finite representation of the narrowing space. In: Proc. of the 23th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2013). Technical Report TR-11-13, Universidad Complutense de Madrid, pp. 113–128 (To appear in Springer LNCS, 2013). http://users.dsic.upv.es/~gvidal/

Noll, T.: A Rewriting Logic Implementation of Erlang. Electr. Notes Theor. Comput. Sci. 44(2), 206–224 (2001)

Noll, T.: Equational Abstractions for Model Checking Erlang Programs. Electr. Notes Theor. Comput. Sci. 118, 145–162 (2005)

Noll, T.G., Fredlund, L., Gurov, D.: The Erlang Verification Tool. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 582–586. Springer, Heidelberg (2001)

Roy, C.K.: Thomas Noll, Banani Roy, and James R. Cordy. Towards automatic verification of Erlang programs by pi-calculus translation. In: Feeley,M., Trinder, P.W. (eds.) Proc. of the 2006 ACM SIGPLAN Workshop on Erlang, pp. 38–50. ACM (2006)

Slagle, J.R.: Automated theorem-proving for theories with simplifiers, commutativity and associativity. Journal of the ACM 21(4), 622–642 (1974)

Svensson, H., Fredlund, L.-A.: A more accurate semantics for distributed Erlang. In: Thompson, S.J., Fredlund. L.-A., (eds.) Proceedings of the 2007 ACM SIGPLAN Workshop on Erlang, pp. 43–54. ACM (2007)

Vidal, G.: Closed symbolic execution for verifying program termination. In: Proc. of the 12th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2012), pp. 34–43. IEEE (2012)

Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)

[-]

recommendations

 

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

Mostrar el registro completo del ítem