Boosting the Reuse of Formal Specifications
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 pe...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , , , , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
Springer Verlag
2018
|
| Materias: | |
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 08893caa a22008897a 4500 | ||
|---|---|---|---|
| 001 | PAPER-25367 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518205724.0 | ||
| 008 | 190410s2018 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-85049896977 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Moscato, M.M. | |
| 245 | 1 | 0 | |a Boosting the Reuse of Formal Specifications |
| 260 | |b Springer Verlag |c 2018 | ||
| 270 | 1 | 0 | |m Moscato, M.M.; National Institute of AerospaceUnited States; email: mariano.moscato@nianet.org |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a 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 | ||
| 504 | |a Burris, S., Sankappanavar, H.P., A Course in Universal Algebra (1981) Graduate Texts in Mathematics, , Springer, Berlin | ||
| 504 | |a Enderton, H.B., (1972) A Mathematical Introduction to Logic, , Academic Press, New York | ||
| 504 | |a 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 | ||
| 504 | |a Troelstra, A.S., Schwichtenberg, H., (1996) Basic Proof Theory. Number 43 in Cambridge Tracts in Theoretical Computer Science, , Cambridge University Press, Cambridge | ||
| 504 | |a Girard, J.Y., Lafont, Y., Taylor, P., (1989) Proofs and Types. Number 7 in Cambridge Tracts in Theoretical Computer Science, , Cambridge University Press, Cambridge | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a McLane, S., (1971) Categories for Working Mathematician, , Graduate Texts in Mathematics. Springer, Berlin | ||
| 504 | |a Pierce, B.C., (1991) Basic Category Theory for Computer Scientists, , MIT Press, Cambridge | ||
| 504 | |a 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 | ||
| 504 | |a Goguen, J.A., Roşu, G., Institution morphisms (2002) Formal Aspects Comput., 13 (3-5), pp. 274-307 | ||
| 504 | |a Turski, W.M., Maibaum, T.S.E., (1987) The Specification of Computer Programs. International Computer Science Series, , Addison-Wesley Publishing Co., Inc., Boston | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Zimmermann, T., Herbelin, H., (2015) Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant, , arXiv preprint arXiv | ||
| 504 | |a Sozeau, M., A new look at generalized rewriting in type theory (2010) J. Formalized Reasoning, 2 (1), pp. 41-62 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Dagand, P.É., Tabareau, N., Tanter, É., Foundations of dependent interoperability (2018) J. Funct. Program., 28A4 - | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a National Institute of Aerospace, Hampton, VA, United States | ||
| 593 | |a Instituto de Investigación En Ciencias de la Computación (ICC), CONICET–Universidad de Buenos Aires, Buenos Aires, Argentina | ||
| 593 | |a NASA Langley Research Center, Hampton, VA, United States | ||
| 650 | 1 | 7 | |2 spines |a ALGEBRA |
| 690 | 1 | 0 | |a COMPUTER CIRCUITS |
| 690 | 1 | 0 | |a FORMAL SPECIFICATION |
| 690 | 1 | 0 | |a NASA |
| 690 | 1 | 0 | |a REUSABILITY |
| 690 | 1 | 0 | |a SPECIFICATION LANGUAGES |
| 690 | 1 | 0 | |a ALGEBRAIC SPECIFICATIONS |
| 690 | 1 | 0 | |a FORMAL DEFINITION |
| 690 | 1 | 0 | |a FORMAL DESCRIPTION |
| 690 | 1 | 0 | |a FORMAL DEVELOPMENT |
| 690 | 1 | 0 | |a FORMAL SYSTEMS |
| 690 | 1 | 0 | |a PROTOTYPE VERIFICATION SYSTEMS |
| 690 | 1 | 0 | |a UNIVERSAL ALGEBRA |
| 690 | 1 | 0 | |a THEOREM PROVING |
| 700 | 1 | |a Lopez Pombo, C.G. | |
| 700 | 1 | |a Muñoz, C.A. | |
| 700 | 1 | |a Feliú, M.A. | |
| 700 | 1 | |a Avigad J. | |
| 700 | 1 | |a Mahboubi A. | |
| 711 | 2 | |d 9 July 2018 through 12 July 2018 |g Código de la conferencia: 215609 | |
| 773 | 0 | |d Springer Verlag, 2018 |g v. 10895 LNCS |h pp. 477-494 |p Lect. Notes Comput. Sci. |n Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |x 03029743 |w (AR-BaUEN)CENRE-983 |z 9783319948201 |t 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-85049896977&doi=10.1007%2f978-3-319-94821-8_28&partnerID=40&md5=3c195006fc85c1f5606635a08b2f1f5c |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1007/978-3-319-94821-8_28 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_03029743_v10895LNCS_n_p477_Moscato |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v10895LNCS_n_p477_Moscato |y Registro en la Biblioteca Digital |
| 961 | |a paper_03029743_v10895LNCS_n_p477_Moscato |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 963 | |a VARI | ||
| 999 | |c 86320 | ||