{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:45Z","timestamp":1725664305243},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601173"},{"type":"electronic","value":"9783540494454"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60117-1_5","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:44:04Z","timestamp":1330278244000},"page":"50-66","source":"Crossref","is-referenced-by-count":4,"title":["Computer-aided computing"],"prefix":"10.1007","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"issue":"4","key":"5_CR1","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W. R. Bevier","year":"1989","unstructured":"William R. Bevier, Warren A. Hunt, Jr., J Strother Moore, and William D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411\u2013428, December 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR2","volume-title":"A Computational Logic Handbook","author":"R. S. Boyer","year":"1988","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, New York, NY, 1988."},{"key":"5_CR3","first-page":"428","volume-title":"Symbolic model checking: 1020 states and beyond","author":"J. R. Burch","year":"1990","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In 5th Annual IEEE Symposium on Logic in Computer Science, pages 428\u2013439, Philadelphia, PA, June 1990. IEEE Computer Society."},{"issue":"2","key":"5_CR4","doi-asserted-by":"crossref","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"},{"issue":"5","key":"5_CR5","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, September 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR6","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986."},{"key":"5_CR7","volume-title":"Proceedings of EUROCAL 85, Linz (Austria)","author":"T. Coquand","year":"1985","unstructured":"T. Coquand and G. P. Huet. Constructions: A higher order proof system for mechanizing mathematics. In Proceedings of EUROCAL 85, Linz (Austria), Berlin, 1985. Springer-Verlag."},{"key":"5_CR8","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/3-540-54834-3_24","volume-title":"VDM '91: Formal Software Development Methods, volume 551 of Lecture Notes in Computer Science","author":"D. Craigen","year":"1991","unstructured":"Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, and Mark Saaltink. EVES: An overview. In S. Prehn and W. J. Toetenel, editors, VDM '91: Formal Software Development Methods, volume 551 of Lecture Notes in Computer Science, pages 389\u2013405, Noordwijkerhout, The Netherlands, October 1991. Springer-Verlag. Volume 1: Conference Contributions."},{"key":"5_CR9","first-page":"287","volume-title":"FZI Publication 4\/94","author":"D. Cyrluk","year":"1994","unstructured":"D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Ramayya Kumar and Thomas Kropf, editors, Preliminary Proceedings of the Second Conference on Theorem Provers in Circuit Design, pages 287\u2013305, Bad Herrenalb (Blackforest), Germany, September 1994. Forschungszentrum Informatik an der Universit\u00e4t Karlsruhe, FZI Publication 4\/94."},{"key":"5_CR10","volume-title":"Technical Report SRI-CSL-95-3","author":"D. Cyrluk","year":"1995","unstructured":"David Cyrluk, Patrick Lincoln, Paliath Narendran, Sam Owre, Sreeranga Ragan, John Rushby, Natarajan Shankar, Jens Ulrik Skakkeb\u00e6k, Mandayam Srivas, and Friedrich von Henke. Seven papers on mechanized formal verification. Technical Report SRI-CSL-95-3, Computer Science Laboratory, SRI International, Menlo Park, CA, January 1995."},{"key":"5_CR11","unstructured":"Dennis Dams, Orna Grumberg, and Rob Gerth. Abstract interpretation of reactive systems: Abstractions preserving \u2200CTL*, \u2203CTL* and CTL*. In Ernst-R\u00fcdiger Olderog, editor, Programming Concepts, Methods and Calculi (PROCOMET '94), pages 561\u2013581, 1994."},{"issue":"5","key":"5_CR12","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"R. A. Millo De","year":"1979","unstructured":"Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and programs. Communications of the ACM, 22(5):271\u2013280, May 1979.","journal-title":"Communications of the ACM"},{"key":"5_CR13","first-page":"84","volume-title":"Efficient model checking in fragments of the propositional mu-calculus","author":"E.A. Emerson","year":"1985","unstructured":"E.A. Emerson and C.L Lei. Efficient model checking in fragments of the propositional 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."},{"issue":"2","key":"5_CR14","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: An interactive mathematical proof system. Journal of Automated Reasoning, 11(2):213\u2013248, October 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR15","first-page":"748","volume-title":"volume 310 of Lecture Notes in Computer Science","author":"S. J. Garland","year":"1988","unstructured":"Stephen J. Garland and John V. Guttag. LP: The Larch prover. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction (CADE), volume 310 of Lecture Notes in Computer Science, pages 748\u2013749, Argonne, IL, May 1988. Springer-Verlag."},{"key":"5_CR16","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"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","year":"1993","key":"5_CR17","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge, UK, 1993."},{"key":"5_CR18","first-page":"120","volume-title":"Real Time Systems Symposium","author":"C. Heitmeyer","year":"1994","unstructured":"Constance Heitmeyer and Nancy Lynch. The generalized railroad crossing: A case study in formal verification of real-time systems. In Real Time Systems Symposium, pages 120\u2013131, San Juan, Puerto Rico, December 1994. IEEE Computer Society."},{"key":"5_CR19","unstructured":"D. Kapur and H. Zhang. RRL: A User's Manual. General Electric Corporate Research and Development, Schenectady, NY, March 1986. Unpublished Manuscript."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, pages 333\u2013354, December 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"5_CR21","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, Boca Raton, FL, 1995. IEEE Computer Society. To appear."},{"key":"5_CR22","unstructured":"Paul S. Miner. Defining the IEEE-854 floating-point standard in PVS. Technical Memorandum 110167, NASA Langley Research Center, 1995."},{"key":"5_CR23","volume-title":"Three volumes: Language, System, and Prover Reference Manuals","author":"S. Owe","year":"1993","unstructured":"S. Owe, N. Shankar, and J. M. Rushby. User Guide for the PVS Specification and Verification System (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993. Three volumes: Language, System, and Prover Reference Manuals."},{"key":"5_CR24","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526602","volume-title":"Logic and Computation: Interactive Proof with Cambridge LCF","author":"L. C. Paulson","year":"1987","unstructured":"L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, Cambridge, England, 1987."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Isabelle: A generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"issue":"3","key":"5_CR26","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G. L. Peterson","year":"1981","unstructured":"G. L. Peterson. Myths about the mutual exclusion problem. Information Processing Letters, 12(3):115\u2013116, 1981.","journal-title":"Information Processing Letters"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification, CAV '95","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, Lecture Notes in Computer Science, Liege, Belgium, June 1995. Springer-Verlag. To appear."},{"key":"5_CR28","volume-title":"Technical Report SRI-CSL-93-8","author":"N. Shankar","year":"1993","unstructured":"N. Shankar. A lazy approach to compositional verification. Technical Report SRI-CSL-93-8, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993."},{"key":"5_CR29","volume-title":"volume 138 of Lecture Notes in Computer Science","author":"R. E. Shostak","year":"1982","unstructured":"R. E. Shostak, R. Schwartz, and P. M. Melliar-Smith. STP: A mechanized logic for specification and verification. In D. Loveland, editor, 6th International Conference on Automated Deduction (CADE), volume 138 of Lecture Notes in Computer Science, New York, NY, 1982. Springer-Verlag."},{"issue":"1","key":"5_CR30","doi-asserted-by":"crossref","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","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60117-1_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:31:58Z","timestamp":1619573518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60117-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601173","9783540494454"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-60117-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}