{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:43:03Z","timestamp":1559331783270},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540665885","type":"print"},{"value":"9783540481188","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48118-4_43","type":"book-chapter","created":{"date-parts":[[2007,11,14]],"date-time":"2007-11-14T01:30:57Z","timestamp":1195003857000},"page":"1758-1777","source":"Crossref","is-referenced-by-count":3,"title":["Formal methods for extensions to CAS"],"prefix":"10.1007","author":[{"given":"Martin N.","family":"Dunstan","sequence":"first","affiliation":[]},{"given":"Tom","family":"Kelsey","sequence":"additional","affiliation":[]},{"given":"Ursula","family":"Martin","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Linton","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"43_CR1","unstructured":"Ballarin, C., Homann, K., AND Calmet, J. Theorems and algorithms: An interface between Isabelle and Maple. In Proceedings of International Symposium on Symbolic and Algebraic Computation (1995), A.H.M. Levelt, Ed., ACM Press, pp. 150\u2013157.","DOI":"10.1145\/220346.220366","doi-asserted-by":"crossref"},{"key":"43_CR2","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1023\/A:1006079212546","volume":"21","author":"A. Bauer","year":"1998","unstructured":"Bauer, A., Clarke, E., AND Zhao, X. Analytica\u2014an experiment in combining theorem proving and symbolic computation. J. Automat. Reason. 21, 3 (1998), 295\u2013325.","journal-title":"J. Automat. Reason"},{"key":"43_CR3","author":"B. Buchberger","first-page":"193","year":"1996","unstructured":"Buchberger, B. Symbolic computation: computer algebra and logic. In Frontiers of combining systems (Munich, 1996). Kluwer Acad. Publ., Dordrecht, 1996, pp. 193\u2013219.","volume-title":"Frontiers of combining systems (Munich, 1996)","DOI":"10.1007\/978-94-009-0349-4_10","doi-asserted-by":"crossref"},{"key":"43_CR4","unstructured":"Char, B. W. Maple V language Reference Manual. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4615-7386-9","doi-asserted-by":"crossref"},{"key":"43_CR5","author":"Y. a. Cheon","year":"1994","unstructured":"Cheon, Y., AND Leavens, G. T. A gentle introduction to Larch\/Smalltalk specification browsers. Tech. Rep. TR 94-01, Department of Computer Science, Iowa State University, 226 Atanaso Hall, Ames, Iowa 50011-1040, USA, Jan. 1994.","series-title":"Tech. Rep. TR 94-01","volume-title":"A gentle introduction to Larch\/Smalltalk specification browsers"},{"key":"43_CR6","unstructured":"Detlefs, D. L. An overview of the Extended Static Checking system. In Proceedings of The First Workshop on Formal Methods in Software Practice (Jan 1996), ACM (SIGSOFT), pp. 1\u20139."},{"key":"43_CR7","unstructured":"Dingle, A., AND Fateman, R. J. Branch cuts in computer algebra. In Symbolic and Algebraic Computation (1994), ISSAC, ACM Press.","DOI":"10.1145\/190347.190424","doi-asserted-by":"crossref"},{"issue":"2","key":"43_CR8","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. a. Dolzmann","year":"1997","unstructured":"Dolzmann, A., AND Sturm, T. REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31, 2 (June 1997), 2\u20139.","journal-title":"ACM SIGSAM Bulletin"},{"key":"43_CR9","unstructured":"Dunstan, M., Kelsey, T., Linton, S., AND Martin, U. Lightweight formal methods for computer algebra systems. In ISSAC (1998).","DOI":"10.1145\/281508.281560","doi-asserted-by":"crossref"},{"key":"43_CR10","author":"D. Evans","year":"1994","unstructured":"Evans, D. Using specifications to check source code. Master\u2019s thesis, Department of Electrical Engineering and Computer Science, MIT Lab. for Computer Science, 545 Technology Square, Cambridge, MA 02139, June 1994.","volume-title":"Master\u2019s thesis, Department of Electrical Engineering and Computer Science"},{"key":"43_CR11","doi-asserted-by":"crossref","first-page":"775","DOI":"10.2140\/pjm.1963.13.775","volume":"13","author":"W. a. Feit","year":"1963","unstructured":"Feit, W., AND Thompson, J. G. Solvability of groups of odd order. Pacific Journal of Mathematics 13 (1963), 775\u20131029.","journal-title":"Pacific Journal of Mathematics"},{"key":"43_CR12","unstructured":"The GAP Group. GAP Groups, Algorithms, and Programming, Version 4. Aachen, St Andrews, 1998. ( http:\/\/www-gap.dcs.st-and.ac.uk\/~gap )."},{"key":"43_CR13","unstructured":"Gordon, M. J. C. Programming language theory and its implementation. Series in Computer Science. Prentice Hall International, 1988."},{"key":"43_CR14","year":"1993","unstructured":"Gordon, M. J. C., AND Melham, T. F., Eds. Introduction to HOL. Cambridge University Press, Cambridge, 1993. A theorem proving environment for higher order logic, Appendix B by R. J. Boulton.","volume-title":"Introduction to HOL"},{"key":"43_CR15","unstructured":"Guaspari, D., Marceau, C., AND Polak, W. Formal verification of Ada programs. In First International Workshop on Larch (July 1992), U. Martin and J. Wing, Eds., Springer-Verlag, pp. 104\u2013141.","DOI":"10.1007\/978-1-4471-3558-6_8","doi-asserted-by":"crossref"},{"key":"43_CR16","unstructured":"Guttag, J. V., AND Horning, J. J. Larch: Languages and Tools for Formal Specification, first ed. Texts and Monograps in Computer Science. Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4612-2704-5","doi-asserted-by":"crossref"},{"key":"43_CR17","unstructured":"Harrison, J., AND Th\u00e9ry, L. Extending the HOL theorem prover with a computer algebra system to reason about the reals. In Higher order logic theorem proving and its applications (Vancouver, BC, 1993). Springer, Berlin, 1994, pp. 174\u2013184.","DOI":"10.1007\/3-540-57826-9_134","doi-asserted-by":"crossref"},{"key":"43_CR18","author":"P. Jackson","year":"1995","unstructured":"Jackson, P. Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, Apr. 1995.","series-title":"PhD thesis","volume-title":"Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra"},{"key":"43_CR19","unstructured":"Jenks, R. D., AND Sutor, R. S. AXIOM. Numerical Algorithms Group Ltd., Oxford, 1992. The scientific computation system, With a foreword by David V. Chudnovsky and Gregory V. Chudnovsky."},{"key":"43_CR20","unstructured":"Jones, C. B. Systematic Software Development using VDM, second ed. Computer Science. Prentice Hall International, 1990."},{"key":"43_CR21","author":"K. D. Jones","year":"1991","unstructured":"Jones, K. D. LM3: a Larch interface language for Modula-3, a definition and introduction. Tech. Rep. 72, SRC, Digital Equipment Corporation, Palo Alto, California, June 1991.","series-title":"Tech. Rep.","volume-title":"LM3: a Larch interface language for Modula-3, a definition and introduction"},{"key":"43_CR22","unstructured":"King, D. J., AND Arthan, R. D. Development of practical verification tools. The ICL Systems Journal 1 (May 1996)."},{"key":"43_CR23","unstructured":"Leavens, G. T., AND Cheon, Y. Preliminary design of Larch\/C+ +. In First International Workshop on Larch (July 1992), U. Martin and J. M. Wing, Eds., Workshops in Computing, Springer-Verlag, pp. 159\u2013184.","DOI":"10.1007\/978-1-4471-3558-6_10","doi-asserted-by":"crossref"},{"key":"43_CR24","unstructured":"Meyer, B. Object-Oriented Software Construction. Computer Science. Prentice Hall International, 1988."},{"key":"43_CR25","author":"S. Owre","year":"1993","unstructured":"Owre, S., Shankar, N., AND Rushby, J. M. User Guide for the PVS Specification and Verification System. Computer Science Laboratory, SRI International, Menlo Park, CA, Feb. 1993.","volume-title":"User Guide for the PVS Specification and Verification System"},{"key":"43_CR26","unstructured":"Poll, E., AND Thompson, S. Adding the axioms to Axiom: Towards a system of automated reasoning in aldor. Technical Report 6-98, Computing Laboratory, University of Kent, May 1998."},{"key":"43_CR27","unstructured":"Potter, B., Sinclair, J., AND Till, D. An introduction to formal specification and Z. Prentice Hall International, 1991."},{"key":"43_CR28","unstructured":"Sannella, D. Formal program development in Extended ML for the working programmer. In Proceedings of the 3rd BCS\/FACS Workshop on Refinement (1990), Springer Workshops in Computing, pp. 99\u2013130."},{"key":"43_CR29","unstructured":"Vandevoorde, M. T., AND Guttag, J. V. Using specialized procedures and specification-based analysis to reduce the runtime costs of modularity. In Proceedings of the 1994 ACM\/SIGSOFT Foundations of Software Engineering Conference (1994).","DOI":"10.1145\/193173.195300","doi-asserted-by":"crossref"},{"key":"43_CR30","unstructured":"Wing, J. M. A two-tiered approach to specifying programs. Tech. Rep. LCS\/TR-299, Laboratory for Computer Science, MIT, May 1983."},{"key":"43_CR31","author":"J. M. Wing","first-page":"297","year":"1992","unstructured":"Wing, J. M., Rollins, E., AND Zaremski, A. M. Thoughts on a Larch\/ML and a new application for TP. In First International Workshop on Larch (July 1992), U. Martin and J. M. Wing, Eds., Workshops in Computing, Springer-Verlag, pp. 297\u2013312.","volume-title":"First International Workshop on Larch"},{"key":"43_CR32","unstructured":"Wolfram, S. Mathematica: A system for doing mathematics by computer, 2 ed. Addison Wesley, 1991."}],"container-title":["FM\u201999 \u2014 Formal Methods","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48118-4_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T11:30:20Z","timestamp":1556969420000},"score":1.0,"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665885","9783540481188"],"references-count":32,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-48118-4_43","relation":{"cites":[]},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}]}}