Navegar

Colección

Datos Estadísticas

Artículo

Moscato, M.M.; Lopez Pombo, C.G.; Muñoz, C.A.; Feliú, M.A.; Avigad J.; Mahboubi A. "Boosting the Reuse of Formal Specifications" (2018) 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018. 10895 LNCS:477-494
El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Advances in theorem proving have enabled the emergence of a variety of formal developments that, over the years, have resulted in large corpuses of formalizations. For example, the NASA PVS Library is a collection of 55 formal developments written in the Prototype Verification System (PVS) over a period of almost 30 years and containing more than 28000 proofs. Unfortunately, the simple accumulation of formal developments does not guarantee their reusability. In fact, in formal systems with very expressive specification languages, it is often the case that a particular conceptual object is defined in different ways. This paper presents a technique to establish sound connections between formal definitions. Such connections support the possibility of (partial) borrowing of proved results from one formal description into another, improving the reusability of formal developments. The technique is described using concepts from the field of universal algebra and algebraic specification. The technique is illustrated with concrete examples taken from formalizations available in the NASA PVS Library. © 2018, Springer International Publishing AG, part of Springer Nature.

Registro:

Documento: Artículo
Título:Boosting the Reuse of Formal Specifications
Autor:Moscato, M.M.; Lopez Pombo, C.G.; Muñoz, C.A.; Feliú, M.A.; Avigad J.; Mahboubi A.
Filiación:National Institute of Aerospace, Hampton, VA, United States
Instituto de Investigación En Ciencias de la Computación (ICC), CONICET–Universidad de Buenos Aires, Buenos Aires, Argentina
NASA Langley Research Center, Hampton, VA, United States
Palabras clave:Algebra; Computer circuits; Formal specification; NASA; Reusability; Specification languages; Algebraic specifications; Formal definition; Formal Description; Formal development; Formal systems; Prototype verification systems; Universal algebra; Theorem proving
Año:2018
Volumen:10895 LNCS
Página de inicio:477
Página de fin:494
DOI: http://dx.doi.org/10.1007/978-3-319-94821-8_28
Título revista:9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v10895LNCS_n_p477_Moscato

Referencias:

  • Owre, S., Rushby, J.M., Shankar, N., PVS: A prototype verification system (1992) CADE 1992. LNCS, 607, pp. 748-752. , Kapur, D. (ed.), Springer, Heidelberg, https://doi.org/10.1007/3-540-55602-8 217
  • Burris, S., Sankappanavar, H.P., A Course in Universal Algebra (1981) Graduate Texts in Mathematics, , Springer, Berlin
  • Enderton, H.B., (1972) A Mathematical Introduction to Logic, , Academic Press, New York
  • van Benthem, J., Doets, K., Higher-order logic (2001) Gabbay, D., Guenthner, F. (Eds.) Handbook of Philosophical Logic, 2Nd Edn., Vol. 1, Pp. 189–243. Kluwer Academic Publishers
  • Troelstra, A.S., Schwichtenberg, H., (1996) Basic Proof Theory. Number 43 in Cambridge Tracts in Theoretical Computer Science, , Cambridge University Press, Cambridge
  • Girard, J.Y., Lafont, Y., Taylor, P., (1989) Proofs and Types. Number 7 in Cambridge Tracts in Theoretical Computer Science, , Cambridge University Press, Cambridge
  • Barendregt, H.P., Lambda calculi with types (1999) Handbook of Logic in Computer Science, Volume II, , Abramsky, S., Gabbay, D., Maibaum, T.S.E. (eds.), Oxford University Press
  • Clausen, M., Fortenbacher, A., Efficient solution of linear diophantine equations (1989) J. Symbolic Comput., 8 (1), pp. 201-216. , https://doi.org/10.1016/S0747-7171(89)80025-2
  • Ehrig, H., Mahr, B., Orejas, F., Introduction to algebraic specification. Part 1: Formal methods for software development (1992) Comput. J., 35 (5), pp. 468-477
  • Ehrig, H., Mahr, B., Orejas, F., Introduction to algebraic specification. Part 2: From classical view to foundations of system specifications (1992) Comput. J., 35 (5), pp. 468-477
  • McLane, S., (1971) Categories for Working Mathematician, , Graduate Texts in Mathematics. Springer, Berlin
  • Pierce, B.C., (1991) Basic Category Theory for Computer Scientists, , MIT Press, Cambridge
  • Meseguer, J., General logics (1989) Ebbinghaus, H.D., Fernandez-Prida, J., Garrido, M., Lascar, D., Artalejo, M.R. (Eds.) Proceedings of the Logic Colloquium 1987, Granada, Spain, North Holland, Vol. 129, Pp. 275–329
  • Goguen, J.A., Roşu, G., Institution morphisms (2002) Formal Aspects Comput., 13 (3-5), pp. 274-307
  • Turski, W.M., Maibaum, T.S.E., (1987) The Specification of Computer Programs. International Computer Science Series, , Addison-Wesley Publishing Co., Inc., Boston
  • Bernstein, S., Démonstration du théorème de weierstrass fondée sur le calcul des probabilités (1912) Commun. Kharkov Math. Soc., 13 (1), pp. 1-2
  • Muñoz, C., Narkawicz, A., Formalization of a representation of Bernstein polynomials and applications to global optimization (2013) J. Autom. Reasoning, 51 (2), pp. 151-196
  • Clausen, M., Fortenbacher, A., Efficient solution of linear diophantine equations (1989) J. Symbolic Comput., 8 (1), pp. 201-216. , https://doi.org/10.1016/S0747-7171(89)80025-2
  • Bertot, Y., Castéran, P., (2013) Interactive Theorem Proving and Program Development: Coqart: The Calculus of Inductive Constructions, , https://doi.org/10.1007/978-3-662-07964-5, Springer, Heidelberg
  • Huffman, B., Kunčar, O., Lifting and transfer: A modular design for quotients in Isabelle/HOL (2013) CPP 2013. LNCS, 8307, pp. 131-146. , Gonthier, G., Norrish, M. (eds.), Springer, Cham, https://doi.org/10.1007/978-3-319-03545-1 9
  • Zimmermann, T., Herbelin, H., (2015) Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant, , arXiv preprint arXiv
  • Sozeau, M., A new look at generalized rewriting in type theory (2010) J. Formalized Reasoning, 2 (1), pp. 41-62
  • Magaud, N., Changing data representation within the Coq system (2003) Tphols 2003. LNCS, 2758, pp. 87-102. , Basin, D., Wolff, B. (eds.), Springer, Heidelberg, https://doi.org/10.1007/10930755 6
  • Clausen, M., Fortenbacher, A., Efficient solution of linear diophantine equations (1989) J. Symbolic Comput., 8 (1), pp. 201-216. , https://doi.org/10.1016/S0747-7171(89)80025-2
  • Lammich, P., Refinement based verification of imperative data structures (2016) Proceedings of the 5Th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pp. 27-36. , ACM, New York
  • Cohen, C., Dénès, M., Mörtberg, A., Refinements for free! (2013) CPP 2013. LNCS, 8307, pp. 147-162. , Gonthier, G., Norrish, M. (eds.), Springer, Cham, https://doi.org/10.1007/978-3-319-03545-1 10
  • Clausen, M., Fortenbacher, A., Efficient solution of linear diophantine equations (1989) J. Symbolic Comput., 8 (1), pp. 201-216. , https://doi.org/10.1016/S0747-7171(89)80025-2
  • Dagand, P.É., Tabareau, N., Tanter, É., Foundations of dependent interoperability (2018) J. Funct. Program., 28A4 -

Citas:

---------- APA ----------
Moscato, M.M., Lopez Pombo, C.G., Muñoz, C.A., Feliú, M.A., Avigad J. & Mahboubi A. (2018) . Boosting the Reuse of Formal Specifications. 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018, 10895 LNCS, 477-494.
http://dx.doi.org/10.1007/978-3-319-94821-8_28
---------- CHICAGO ----------
Moscato, M.M., Lopez Pombo, C.G., Muñoz, C.A., Feliú, M.A., Avigad J., Mahboubi A. "Boosting the Reuse of Formal Specifications" . 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 10895 LNCS (2018) : 477-494.
http://dx.doi.org/10.1007/978-3-319-94821-8_28
---------- MLA ----------
Moscato, M.M., Lopez Pombo, C.G., Muñoz, C.A., Feliú, M.A., Avigad J., Mahboubi A. "Boosting the Reuse of Formal Specifications" . 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018, vol. 10895 LNCS, 2018, pp. 477-494.
http://dx.doi.org/10.1007/978-3-319-94821-8_28
---------- VANCOUVER ----------
Moscato, M.M., Lopez Pombo, C.G., Muñoz, C.A., Feliú, M.A., Avigad J., Mahboubi A. Boosting the Reuse of Formal Specifications. Lect. Notes Comput. Sci. 2018;10895 LNCS:477-494.
http://dx.doi.org/10.1007/978-3-319-94821-8_28