{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:38:06Z","timestamp":1743043086930,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357459"},{"type":"electronic","value":"9783642357466"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35746-6_4","type":"book-chapter","created":{"date-parts":[[2012,12,13]],"date-time":"2012-12-13T20:38:40Z","timestamp":1355431120000},"page":"96-132","source":"Crossref","is-referenced-by-count":1,"title":["Advanced Theorem Proving Techniques in PVS and Applications"],"prefix":"10.1007","author":[{"given":"C\u00e9sar A.","family":"Mu\u00f1oz","sequence":"first","affiliation":[]},{"given":"Ramiro A.","family":"Demasi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Archer, M., Vito, B.D., Mu\u00f1oz, C.: Developing user strategies in PVS: A tutorial. In: Proceedings of Design and Application of Strategies\/Tactics in Higher Order Logics STRATA 2003. NASA\/CP-2003-212448, NASA LaRC, Hampton VA 23681-2199, USA (September 2003)"},{"key":"4_CR2","unstructured":"Crow, J., Owre, S., Rushby, J., Shankar, N., Stringer-Calvert, D.: Evaluating, testing, and animating PVS specifications. Tech. rep., Computer Science Laboratory, SRI International, Menlo Park, CA (March 2001)"},{"issue":"2","key":"4_CR3","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1109\/TC.2008.213","volume":"58","author":"M. Daumas","year":"2009","unstructured":"Daumas, M., Lester, D., Mu\u00f1oz, C.: Verified real number calculations: A library for interval arithmetic. IEEE Transactions on Computers\u00a058(2), 226\u2013237 (2009)","journal-title":"IEEE Transactions on Computers"},{"key":"4_CR4","unstructured":"Di Vito, B.: A PVS prover strategy package for common manipulations. Technical Memorandum NASA\/TM-2002-211647, NASA Langley Research Center (2002)"},{"key":"4_CR5","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-28891-3_30","volume-title":"NASA Formal Methods","author":"L. Lensink","year":"2012","unstructured":"Lensink, L., Smetsers, S., van Eekelen, M.: Generating Verifiable Java Code from Verified PVS Specifications. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 310\u2013325. Springer, Heidelberg (2012)"},{"key":"4_CR7","unstructured":"L\u00fcttgen, G., Mu\u00f1oz, C., Butler, R., Vito, B.D., Miner, P.: Towards a customizable PVS. Contractor Report NASA\/CR-2000-209851, ICASE, Langley Research Center, Hampton VA 23681-2199, USA (January 2000)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/11817963_36","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"2006","unstructured":"Manolios, P., Vroon, D.: Termination Analysis with Calling Context Graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 401\u2013414. Springer, Heidelberg (2006)"},{"key":"4_CR9","unstructured":"Mu\u00f1oz, C.: Rapid prototyping in PVS. Contractor Report NASA\/CR-2003-212418, NASA, Langley Research Center, Hampton VA 23681-2199, USA (May 2003)"},{"key":"4_CR10","unstructured":"Mu\u00f1oz, C.: Batch proving and proof scripting in PVS. Report NIA Report No. 2007-03, NASA\/CR-2007-214546, NIA-NASA Langley, National Institute of Aerospace, Hampton, VA (February 2007)"},{"key":"4_CR11","unstructured":"Mu\u00f1oz, C., Mayero, M.: Real automation in the field. Contractor Report NASA\/CR-2001-211271, ICASE, Langley Research Center, Hampton VA 23681-2199, USA (December 2001)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C., Narkawicz, A.: Formalization of a representation of Bernstein polynomials and applications to global optimization. Journal of Automated Reasoning (2012) (accepted for publication)","DOI":"10.1007\/s10817-012-9256-3"},{"key":"4_CR13","unstructured":"Nipkow, S.B.T.: Random testing in Isabelle\/HOL. In: Cuellar, J., Liu, Z. (eds.) Software Engineering and Formal Methods (SEFM 2004), pp. 230\u2013239. IEEE Computer Society (2004)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"4_CR15","unstructured":"Owre, S., Shankar, N.: Abstract datatypes in PVS. Contractor Report NASA\/CR-97-206264, NASA, Langley Research Center, Hampton VA 23681-2199, USA (November 1997)"},{"key":"4_CR16","unstructured":"Owre, S., Shankar, N.: The formal semantics of PVS. Technical Report CSL-97-2, Computer Science Laboratory, SRI International (March 1999)"},{"key":"4_CR17","unstructured":"Owre, S., Shankar, N.: Theory interpretations in PVS. Technical report, SRI International, Menlo Park, CA (April 2001)"},{"issue":"9","key":"4_CR18","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J. Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering\u00a024(9), 709\u2013720 (1998), \n                  \n                    http:\/\/www.csl.sri.com\/papers\/tse98\/","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR19","unstructured":"Shankar, N.: Efficiently executing PVS. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (November 1999)"}],"container-title":["Lecture Notes in Computer Science","Tools for Practical Software Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35746-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:36:54Z","timestamp":1558301814000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35746-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642357459","9783642357466"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35746-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}