{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:30:35Z","timestamp":1775053835689,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540614746","type":"print"},{"value":"9783540685999","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_91","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:41:41Z","timestamp":1330292501000},"page":"411-414","source":"Crossref","is-referenced-by-count":181,"title":["PVS: Combining specification, proof checking, and model checking"],"prefix":"10.1007","author":[{"given":"S.","family":"Owre","sequence":"first","affiliation":[]},{"given":"S.","family":"Rajan","sequence":"additional","affiliation":[]},{"given":"J. M.","family":"Rushby","sequence":"additional","affiliation":[]},{"given":"N.","family":"Shankar","sequence":"additional","affiliation":[]},{"given":"M.","family":"Srivas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"issue":"2","key":"39_CR1","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"39_CR2","first-page":"84","volume-title":"Efficient model checking in fragments of the prepositional mu-calculus","author":"E.A. Emerson","year":"1985","unstructured":"E.A. Emerson and C.L. Lei. Efficient model checking in fragments of the prepositional mu-calculus. In Proceedings of the 10th Symposium on Principles of Programming Languages, pages 84\u201396, New Orleans, LA, January 1985. Association for Computing Machinery."},{"key":"39_CR3","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"39_CR4","unstructured":"G. L. J. M. Janssen. ROBDD Software. Department of Electrical Engineering, Eindhoven University of Technology, October 1993."},{"key":"39_CR5","first-page":"2","volume-title":"Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods","author":"S. P. Miller","year":"1995","unstructured":"Steven P. Miller and Mandayam Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, pages 2\u201316, Boca Raton, FL, 1995. IEEE Computer Society."},{"key":"39_CR6","unstructured":"Paul S. Miner. Defining the IEEE-854 floating-point standard in PVS. Technical Memorandum 110167, NASA Langley Research Center, 1995."},{"issue":"2","key":"39_CR7","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"39_CR8","first-page":"84","volume-title":"Computer-Aided Verification, CAV '95, volume 939 of Lecture Notes in Computer Science","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Pierre Wolper, editor, Computer-Aided Verification, CAV '95, volume 939 of Lecture Notes in Computer Science, pages 84\u201397, Liege, Belgium, June 1995. Springer-Verlag."},{"key":"39_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification, CAV '96","author":"H. Ruess","year":"1996","unstructured":"H. Ruess, M. K. Srivas, and N. Shankar. Modular verification of SRT division. In Rajeev Alur and Tom Henzinger, editors, Computer-Aided Verification, CAV '96, Lecture Notes in Computer Science, New Brunswick, NJ, July 1996. Springer-Verlag. To appear."},{"issue":"1","key":"39_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1\u201312, January 1984.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_91.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:32:18Z","timestamp":1619573538000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_91"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_91","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}