{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:20:51Z","timestamp":1747592451532},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540406648"},{"type":"electronic","value":"9783540451303"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_11","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T11:27:09Z","timestamp":1150716429000},"page":"171-187","source":"Crossref","is-referenced-by-count":11,"title":["Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover"],"prefix":"10.1007","author":[{"given":"Hasan","family":"Amjad","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Combining theorem proving and trajectory evaluation in an industrial environment. In: Design Automation Conference (DAC), pp. 538\u2013541. ACM\/IEEE (1998)","DOI":"10.1145\/277044.277189"},{"key":"11_CR2","unstructured":"Agerholm, S., Skjodt, H.: Automating a model checker for recursive modal assertions in HOL. Technical Report 92, Aarhus University (January 1990)"},{"issue":"3","key":"11_CR3","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"key":"11_CR4","unstructured":"The BuDDy ROBDD Package (2002), \n                    \n                      http:\/\/www.itu.dk\/research\/buddy"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Representing circuits more efficiently in symbolic model checking. In: Proceedings of the ACM Design Automation Conference (1991)","DOI":"10.1145\/127601.127702"},{"issue":"2","key":"11_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05(2), 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45657-0_20","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2002","unstructured":"Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstractionrefinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 265. Springer, Heidelberg (2002)"},{"key":"11_CR8","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)"},{"issue":"5","key":"11_CR9","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR10","unstructured":"Cleaveland, R.: Tableau-based model checking in the propostional mu-calculus. Extended Abstract, Computer Science Department, University of Sussex (1988)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Formal Methods in Computer-Aided Design (November 2002)","DOI":"10.1007\/3-540-36126-X_2"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-60045-0_40","volume-title":"Proceedings of the 1995 Workshop on Computer Aided Verification","author":"J. Dingel","year":"1995","unstructured":"Dingel, J., Filkorn, T.: Model checking for infinite state systems using data abtraction, assumption-commitment style reasoning and theorem proving. In: Proceedings of the 1995 Workshop on Computer Aided Verification. LNCS, vol.\u00a0939, pp. 54\u201369. Springer, Heidelberg (1995)"},{"key":"11_CR13","first-page":"267","volume-title":"1st Annual Symposium on Logic in Computer Science","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: 1st Annual Symposium on Logic in Computer Science, pp. 267\u2013278. IEEE Computer Society Press, Los Alamitos (1986)"},{"key":"11_CR14","first-page":"193","volume-title":"Proceedings of the 14th Logic in Computer Science Conference","author":"M.P. Fiore","year":"1999","unstructured":"Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Proceedings of the 14th Logic in Computer Science Conference, pp. 193\u2013202. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"11_CR15","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing, Special issue in honour of Rod Burstall (2001)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"A.D. Gordon","year":"1996","unstructured":"Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125. Springer, Heidelberg (1996)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C.: Programming combinations of deduction and bdd-based symbolic calculation. LMS Journal of Computation and Mathematics (August 2002)","DOI":"10.1112\/S1461157000000693"},{"key":"11_CR18","volume-title":"Introduction to HOL (A theorem-proving environment for higher order logic)","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, Cambridge (1993)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"11_CR20","unstructured":"The HOL Proof Tool (2003), \n                    \n                      http:\/\/hol.sf.net"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","first-page":"385","volume-title":"Computer Aided Verification","author":"G.J. Holzmann","year":"1996","unstructured":"Holzmann, G.J., Peled, D.: The state of spin. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 385\u2013389. Springer, Heidelberg (1996)"},{"key":"11_CR22","unstructured":"SRI International. Prototype verification system, \n                    \n                      http:\/\/pvs.csl.sri.com"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","first-page":"185","volume-title":"Higher Order Logic Theorem Proving and its Applications","author":"J. Joyce","year":"1993","unstructured":"Joyce, J., Seger, C.: The HOL-Voss system: Model checking inside a generalpurpose theorem prover. In: Higher Order Logic Theorem Proving and its Applications. LNCS, vol.\u00a0780, pp. 185\u2013198. Springer, Heidelberg (1993)"},{"key":"11_CR24","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-56922-7_14","volume-title":"Computer Aided Verification","author":"R.P. Kurshan","year":"1993","unstructured":"Kurshan, R.P., Lamport, L.: Verification of a multiplier: 64 bits and beyond. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 166\u2013180. Springer, Heidelberg (1993)"},{"key":"11_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: Pvs: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rua, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (2001)","DOI":"10.1007\/3-540-45319-9_7"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Rajan","year":"1995","unstructured":"Rajan, S., Shankar, N., Srivas, M.K.: An integration of model checking and automated proof checking. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939. Springer, Heidelberg (1995)"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Saidi, H.: Model checking guided abstraction and analysis. In: Proceedings of the 7th International Static Analysis Symposium (2000)","DOI":"10.1007\/978-3-540-45099-3_20"},{"key":"11_CR31","unstructured":"Seger, C.-J.H.: Voss - a formal hardware verification system: User\u2019s guide. Technical report, The University of British Columbia, UBC-TR-93-45 (December 1993)"},{"key":"11_CR32","unstructured":"Skolem, T.: Some remarks on axiomatised set theory. In: van Heijenoort, J. (ed.) From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931, pp. 290\u2013301. Harvard University Press (1967)"},{"key":"11_CR33","unstructured":"Sprenger, C.: Deductive Local Model Checking. PhD thesis, Computer Networking Laboratory,Swiss Federal Institute of Technology, Lausanne, Switzerland (2000)"},{"key":"11_CR34","unstructured":"Stanford Temporal Prover, \n                    \n                      http:\/\/www-step.stanford.edu"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","volume-title":"TAPSOFT \u201989. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, March 13-17, 1989","author":"C. Stirling","year":"1989","unstructured":"Stirling, C., Walker, D.J.: Local model checking in the modal mu-calculus. In: D\u00edaz, J., Orejas, F. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol.\u00a0351. Springer, Heidelberg (1989)"},{"key":"11_CR36","unstructured":"Symbolic Model Prover, \n                    \n                      http:\/\/www.cs.cmu.edu\/~modelcheck\/symp.html"},{"key":"11_CR37","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics\u00a05, 285\u2013309 (1955)","journal-title":"Pacific Journal of Mathematics"},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/10720084_11","volume-title":"Frontiers of Combining Systems","author":"T.E. Uribe","year":"2000","unstructured":"Uribe, T.E.: Combinations of model checking and theorem proving. In: Kirchner, H. (ed.) FroCos 2000. LNCS, vol.\u00a01794, pp. 151\u2013170. Springer, Heidelberg (2000)"},{"key":"11_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035797","volume-title":"Automata, Languages and Programming","author":"G. Winskel","year":"1989","unstructured":"Winskel, G.: A note on model checking in the modal \u03bd-calculus. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372. Springer, Heidelberg (1989)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10930755_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,14]],"date-time":"2019-03-14T20:58:51Z","timestamp":1552597131000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/10930755_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}