{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:50:44Z","timestamp":1754484644189},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_42","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:37:39Z","timestamp":1330277859000},"page":"84-97","source":"Crossref","is-referenced-by-count":75,"title":["An integration of model checking with automated proof checking"],"prefix":"10.1007","author":[{"given":"S.","family":"Rajan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N.","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. K.","family":"Srivas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Julian Bradfield and Colin Stirling. Verifying temporal properties of processes. In J. C. M. Baeten and J. W. Klop, editors, CONCUR '90, number 458 in Lecture Notes in Computer Science, pages 115\u2013125. Springer Verlag, 1990.","DOI":"10.1007\/BFb0039055"},{"issue":"4","key":"8_CR2","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design, 13(4):401\u2013424, April 1994.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"issue":"2","key":"8_CR3","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":"8_CR4","series-title":"volume 818 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer-Aided Verification 94","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In David Dill, editor, Computer-Aided Verification 94, volume 818 of Lecture Notes in Computer Science, pages 415\u2013427, Stanford, CA, June 1994. Springer Verlag."},{"issue":"5","key":"8_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":"8_CR6","unstructured":"R. Cleaveland. Tableau-based model checking in the prepositional mu-calculus. Technical Report 2\/89, University of Sussex, March 1989."},{"key":"8_CR7","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."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Dingel and Thomas Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In Computer-Aided Verification 95, 1995. This volume.","DOI":"10.1007\/3-540-60045-0_40"},{"key":"8_CR9","series-title":"volume B: Formal Models and Semantics","first-page":"995","volume-title":"Handbook of Theoretical Computer Science","author":"E. A. Emerson","year":"1990","unstructured":"E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 16, pages 995\u20131072. Elsevier and MIT press, Amsterdam, The Netherlands, and Cambridge, MA, 1990."},{"key":"8_CR10","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."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Urban Engberg, Peter Gr\u00f8nning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In G. v. Bochmann and D. K. Probst, editors, Computer-Aided Verification 92, number 663 in Lecture Notes in Computer Science, pages 44\u201355. Springer Verlag, 1992.","DOI":"10.1007\/3-540-56496-9_5"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","year":"1993","key":"8_CR12","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":"8_CR13","doi-asserted-by":"crossref","unstructured":"Susanne Graf. Verification of a distributed cache memory by using abstractions. In David L. Dill, editor, Computer-Aided Verification 94, number 818 in Lecture Notes in Computer Science, pages 207\u2013219. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_55"},{"key":"8_CR14","unstructured":"G. Janssen. ROBDD Software. Department of Electrical Engineering, Eindhoven University of Technology, October 1993."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Jeffrey J. Joyce and Carl-Johan H. Seger. Linking Bdd-based symbolic evaluation to interactive theorem proving. In Proceedings of the 30th Design Automation Conference. Association for Computing Machinery, 1993.","DOI":"10.1145\/157485.164981"},{"key":"8_CR16","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":"8_CR17","series-title":"volume 697 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-56922-7_14","volume-title":"Computer-Aided Verification93","author":"R. Kurshan","year":"1993","unstructured":"R. Kurshan and L. Lamport. Verification of a multiplier: 64 bits and beyond. In Costas Courcoubetis, editor, Computer-Aided Verification93, volume 697 of Lecture Notes in Computer Science, pages 166\u2013179, Elounda, Greece, June\/July 1993. Springer Verlag."},{"key":"8_CR18","volume-title":"Automata-Theoretic Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1993","unstructured":"R.P. Kurshan. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1993."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In 8th ACM Symposium on Principles of Distributed Computing, pages 239\u2013248, Edmonton, Alberta, Canada, August 1989.","DOI":"10.1145\/72981.72998"},{"key":"8_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1993."},{"key":"8_CR21","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":"8_CR22","doi-asserted-by":"crossref","unstructured":"Olaf M\u00fcller and Tobias Nipkow. Combining model checking and deduction for I\/O automata. Draft manuscript, 1995.","DOI":"10.1007\/3-540-60630-0_1"},{"key":"8_CR23","first-page":"748","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752, Saratoga, NY, June 1992. Springer-Verlag."},{"key":"8_CR24","unstructured":"D. Park. Finiteness is mu-effable. Technical Report 3, The University of Warwick, March 1989. Theory of Computation Report."},{"key":"8_CR25","first-page":"68","volume-title":"volume 407 of Lecture Notes in Computer Science","author":"P. Wolper","year":"1989","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In J. Sifakis, editor, International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 68\u201380, Grenoble, France, June 1989. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_42.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:28:49Z","timestamp":1605648529000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}