{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:33:58Z","timestamp":1781238838224,"version":"3.54.1"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,3,13]],"date-time":"2010-03-13T00:00:00Z","timestamp":1268438400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2011,6]]},"DOI":"10.1007\/s10817-010-9169-y","type":"journal-article","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T17:56:06Z","timestamp":1268416566000},"page":"1-16","source":"Crossref","is-referenced-by-count":4,"title":["The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4"],"prefix":"10.1007","volume":"47","author":[{"given":"Michael J. C.","family":"Gordon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sandip","family":"Ray","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,3,13]]},"reference":[{"key":"9169_CR1","volume-title":"Model-Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model-Checking. The MIT Press, Cambridge, MA (2000)"},{"key":"9169_CR2","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C., Hunt, W.A., Jr., Kaufmann, M., Reynolds, J.: An embedding of the ACL2 logic in HOL. In: Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), pp. 40\u201346. ACM, August 2006","DOI":"10.1145\/1217975.1217984"},{"key":"9169_CR3","first-page":"153","volume-title":"Proceedings on the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD-2006)","author":"MJC Gordon","year":"2006","unstructured":"Gordon, M.J.C., Hunt, W.A., Jr., Kaufmann, M., Reynolds, J.: An integration of HOL and ACL2. In: Gupta, A., Manolios, P. (eds.) Proceedings on the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD-2006), pp. 153\u2013160. IEEE Computer Society Press, Washington (2006)"},{"key":"9169_CR4","volume-title":"Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge, UK (1993)"},{"key":"9169_CR5","first-page":"49","volume-title":"Towards Verified Systems. Real-Time Safety Critical Systems, vol. 2, chapter 3","author":"MJC Gordon","year":"1994","unstructured":"Gordon, M.J.C., Pitts, A.M.: The HOL logic and system. In: Bowen, J. (ed.) Towards Verified Systems. Real-Time Safety Critical Systems, vol. 2, chapter 3, pp. 49\u201370. Elsevier, Amsterdam (1994)"},{"key":"9169_CR6","unstructured":"Greve, D., Richards, R., Wiliding, M.: A summary of intrinsic partitioning verification. In: Kaufmann, M., Moore, J.S. (eds.) 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, November 2004"},{"key":"9169_CR7","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"9169_CR8","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-45620-1_10","volume-title":"Proceedings of the 18th International Conference on Automated Deduction (CADE 2002)","author":"J Hurd","year":"2002","unstructured":"Hurd, J.: An LCF-style interface between HOL and first-order logic. In: Voronkov, A. (ed.) Proceedings of the 18th International Conference on Automated Deduction (CADE 2002). LNCS, vol. 2392, pp. 134\u2013138. Springer, Berlin, July (2002)"},{"key":"9169_CR9","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge, UK (2004)"},{"key":"9169_CR10","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer, Boston (2000)"},{"key":"9169_CR11","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Boston (2000)"},{"key":"9169_CR12","unstructured":"Kaufmann, M., Moore, J.S.: A Precise Description of the ACL2 Logic. http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/km97.ps.gz (1997)"},{"issue":"2","key":"9169_CR13","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M Kaufmann","year":"2001","unstructured":"Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic. J. Autom. Reason. 26(2), 161\u2013203 (2001)","journal-title":"J. Autom. Reason."},{"key":"9169_CR14","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Moore, J.S.: An ACL2 tutorial. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). LNCS, vol. 5170, pp. 17\u201321. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_4"},{"key":"9169_CR15","unstructured":"Kaufmann, M., Moore, J.S.: The ACL2 Home Page. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/ (2009)"},{"key":"9169_CR16","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"RP Kurshan","year":"1995","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1995)"},{"issue":"3","key":"9169_CR17","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/j.scico.2004.07.004","volume":"57","author":"H Liu","year":"2005","unstructured":"Liu, H., Moore, J.S.: Executable JVM model for analytical reasoning: a study. Sci Comput Program 57(3), 253\u2013274 (2005)","journal-title":"Sci Comput Program"},{"key":"9169_CR18","unstructured":"Norrish, M., Slind, K.L.: The HOL4 Home Page. http:\/\/hol.sourceforge.net\/ (2009)"},{"key":"9169_CR19","unstructured":"Ray, S., Matthews, J., Tuttle, M.: Certifying compositional model checking algorithms in ACL2. In: Hunt, W.A., Jr., Kaufmann, M., Moore, J.S. (eds.) 4th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2003), Boulder, CO, July 2003"},{"key":"9169_CR20","volume-title":"Mathematical Logic","author":"JR Shoenfield","year":"1967","unstructured":"Shoenfield, J.R.: Mathematical Logic. Adison-Wesley, Reading (1967)"},{"key":"9169_CR21","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008)","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). LNCS, vol. 5170, pp. 28\u201332. Springer, Berlin (2008)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9169-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9169-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9169-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T23:56:18Z","timestamp":1685490978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9169-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3,13]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["9169"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9169-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3,13]]}}}