{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:43:53Z","timestamp":1750308233426,"version":"3.41.0"},"reference-count":14,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1985,8,1]],"date-time":"1985-08-01T00:00:00Z","timestamp":491702400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[1985,8]]},"abstract":"<jats:p>This position paper describes a hardware and software verification effort at Argonne National Laboratory based upon the LMA (Logic Machine Architecture) collection of Pascal procedures. The reasoning component of the system is the Interactive Theorem Prover (ITP), a Pascal program using the procedures of LMA. ITP is in effect an enhanced portable implementation of our previous reasoning system AURA. A verification condition generator for the software will be developed using tools such as the TAMPR program transformation system. The resulting system is being applied to prove claims about hardware\/software used in a control system running on a fault-tolerant computer.<\/jats:p>","DOI":"10.1145\/1012497.1012520","type":"journal-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:39:09Z","timestamp":1097170749000},"page":"61-62","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Position paper to be presented at \"Verification workshop III (verkshop III)\" to be held in Watsonville, CA. Feb. 18--21, 1985"],"prefix":"10.1145","volume":"10","author":[{"given":"Brian T.","family":"Smith","sequence":"first","affiliation":[{"name":"Argonne National Laboratory, Argonne, Illinois"}]}],"member":"320","published-online":{"date-parts":[[1985,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"J. Lueger, and L. Goecke","author":"Boyle J. M.","year":"1980","unstructured":"Boyle , J. M. , \" Program adaption and program transformation,\" in Practice in Software Adaption and Maintenance , ed, R. Ehert , J. Lueger, and L. Goecke , North Holland Publishing Co. ( 1980 ). Boyle, J. M., \"Program adaption and program transformation,\" in Practice in Software Adaption and Maintenance, ed, R. Ehert, J. Lueger, and L. Goecke, North Holland Publishing Co. (1980)."},{"key":"e_1_2_1_2_1","first-page":"178","volume-title":"Automated synthesis of combinational logic using theorem proving techniques,\" Proceedings of the Twelfth International Symposium on Multiple-Valued Logic","author":"Kabat W.","year":"1982","unstructured":"Kabat , W. and Wojcik , A. , \" Automated synthesis of combinational logic using theorem proving techniques,\" Proceedings of the Twelfth International Symposium on Multiple-Valued Logic , Paris, France ( May 1982 ), IEEE , pp. 178 -- 199 . Kabat, W. and Wojcik, A., \"Automated synthesis of combinational logic using theorem proving techniques,\" Proceedings of the Twelfth International Symposium on Multiple-Valued Logic, Paris, France (May 1982), IEEE, pp. 178--199."},{"key":"e_1_2_1_3_1","unstructured":"Kljaich J. Ph.D thesis Department of Computer Science IIT in preparation.  Kljaich J. Ph.D thesis Department of Computer Science IIT in preparation."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Lusk E. McCune W.\n     and \n      Overbeek R. \"\n  Logic machine architecture: kernel functions \" 6th Conference on Automated Deduction Vol. \n  138 Lecture Notes in Computer Science ed. \n  D. W. Loveland Springer-Verlag Berlin Heidelberg New\n   York (\n  1982\n  ) pp. \n  70\n  --\n  84\n  .   Lusk E. McCune W. and Overbeek R. \"Logic machine architecture: kernel functions \" 6th Conference on Automated Deduction Vol. 138 Lecture Notes in Computer Science ed. D. W. Loveland Springer-Verlag Berlin Heidelberg New York (1982) pp. 70--84.","DOI":"10.1007\/BFb0000052"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Lusk E. McCune W.\n     and \n      Overbeek R. \"\n  Logic machine architecture: inference mechanisms \" 6th Conference on Automated Deduction Vol. \n  138 Lecture Notes in Computer Science ed. \n  D. W. Loveland Springer-Verlag Berlin Heidelberg New\n   York (\n  1982\n  ) pp. \n  85\n  --\n  108\n  .   Lusk E. McCune W. and Overbeek R. \"Logic machine architecture: inference mechanisms \" 6th Conference on Automated Deduction Vol. 138 Lecture Notes in Computer Science ed. D. W. Loveland Springer-Verlag Berlin Heidelberg New York (1982) pp. 85--108.","DOI":"10.1007\/BFb0000053"},{"key":"e_1_2_1_7_1","volume-title":"Petri Net Theory and the Modeling of Systems","author":"Peterson J. L.","year":"1981","unstructured":"Peterson , J. L. , Petri Net Theory and the Modeling of Systems , Prentice-Hall, Inc. ( 1981 ). Peterson, J. L., Petri Net Theory and the Modeling of Systems, Prentice-Hall, Inc. (1981)."},{"key":"e_1_2_1_8_1","first-page":"251","volume-title":"Automated Generation of Models and Counterexamples and its Application to Open Questions in Ternary Boolean Algebra,\" in Proceedings of the Eighth International Symposium on Multiple-Valued Logic","author":"Winker S.","year":"1978","unstructured":"Winker , S. , and Wos , L. , \" Automated Generation of Models and Counterexamples and its Application to Open Questions in Ternary Boolean Algebra,\" in Proceedings of the Eighth International Symposium on Multiple-Valued Logic , Rosemont, Illinois , IEEE and ACM publication, pp. 251 -- 256 ( 1978 ). Winker, S., and Wos, L., \"Automated Generation of Models and Counterexamples and its Application to Open Questions in Ternary Boolean Algebra,\" in Proceedings of the Eighth International Symposium on Multiple-Valued Logic, Rosemont, Illinois, IEEE and ACM publication, pp. 251--256 (1978)."},{"key":"e_1_2_1_9_1","first-page":"533","article-title":"Semigroups, antiautomorphisms, and involutions: a computer solution to an open problem, I","volume":"37","author":"Winker S.","year":"1981","unstructured":"Winker , S. , Wos , L. , and Lusk , E ., \" Semigroups, antiautomorphisms, and involutions: a computer solution to an open problem, I ,\" Mathematics of Computation , Vol. 37 , pp. 533 -- 545 ( 1981 ). Winker, S., Wos, L., and Lusk, E., \"Semigroups, antiautomorphisms, and involutions: a computer solution to an open problem, I,\" Mathematics of Computation, Vol. 37, pp. 533--545 (1981).","journal-title":"Mathematics of Computation"},{"key":"e_1_2_1_10_1","first-page":"32","article-title":"Automated design of multiple-valued logic circuits by automatic theorem proving techniques","author":"Wojciechowski W.","year":"1983","unstructured":"Wojciechowski , W. and Wojcik , A ., \" Automated design of multiple-valued logic circuits by automatic theorem proving techniques ,\" IEEE Transactions on Computers , Vol. C - 32 , Number 9 ( September 1983 ). Wojciechowski, W. and Wojcik, A., \"Automated design of multiple-valued logic circuits by automatic theorem proving techniques,\" IEEE Transactions on Computers, Vol. C-32, Number 9 (September 1983).","journal-title":"IEEE Transactions on Computers"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/800032.800668"},{"key":"e_1_2_1_12_1","volume-title":"A Formal Design Verification System Based on an Automated Reasoning System,\" Proceedings of the 21st Design Automation Conference (June","author":"Wojcik A.","year":"1984","unstructured":"Wojcik , A. , Srinivas , N. and Kljaich , J. , \" A Formal Design Verification System Based on an Automated Reasoning System,\" Proceedings of the 21st Design Automation Conference (June 1984 ). Wojcik, A., Srinivas, N. and Kljaich, J., \"A Formal Design Verification System Based on an Automated Reasoning System,\" Proceedings of the 21st Design Automation Conference (June 1984)."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093870311"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(84)90054-7"},{"key":"e_1_2_1_15_1","first-page":"316","volume-title":"Proceedings of the 7th \"The Linked Inference Principle, II: The User's Viewpoint,\" in Proceedings of the 7th International Conference on Automated Deduction","volume":"170","author":"Wos L.","year":"1984","unstructured":"Wos , L. , Veroff , R. , Smith , B. , and McCune , W. , in Proceedings of the 7th \"The Linked Inference Principle, II: The User's Viewpoint,\" in Proceedings of the 7th International Conference on Automated Deduction , Vol. 170 , Lecture Notes in Computer Science, ed. R. E. Shostak, Springer-Verlag, New York , pp. 316 -- 332 ( 1984 ). Wos, L., Veroff, R., Smith, B., and McCune, W., in Proceedings of the 7th \"The Linked Inference Principle, II: The User's Viewpoint,\" in Proceedings of the 7th International Conference on Automated Deduction, Vol. 170, Lecture Notes in Computer Science, ed. R. E. Shostak, Springer-Verlag, New York, pp. 316--332 (1984)."}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1012497.1012520","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1012497.1012520","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:43Z","timestamp":1750264303000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1012497.1012520"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985,8]]},"references-count":14,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1985,8]]}},"alternative-id":["10.1145\/1012497.1012520"],"URL":"https:\/\/doi.org\/10.1145\/1012497.1012520","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[1985,8]]},"assertion":[{"value":"1985-08-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}