{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:27Z","timestamp":1725663807884},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578260"},{"type":"electronic","value":"9783540483465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_121","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:26:08Z","timestamp":1330262768000},"page":"1-15","source":"Crossref","is-referenced-by-count":10,"title":["Program verification using HOL-UNITY"],"prefix":"10.1007","author":[{"given":"Flemming","family":"Andersen","sequence":"first","affiliation":[]},{"given":"Kim Dam","family":"Petersen","sequence":"additional","affiliation":[]},{"given":"Jimmi S.","family":"Pettersson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"1_CR1","volume-title":"Master's thesis","author":"S. Agerholm","year":"1991","unstructured":"S. Agerholm. Mechanizing Program Verification in HOL. Master's thesis, Computer Science Department, University of \u00c5rhus, Denmark, September 1991."},{"key":"1_CR2","unstructured":"F. Andersen. A Definitional Theory of UNITY in HOL. In Summary of talks at the Third Annual HOL User Meeting, PB 340, pages 151\u2013162. DAIMI, \u00c5rhus University, October 1990."},{"key":"1_CR3","unstructured":"F. Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, 1992. Also published as TFL RT 1992\u20133."},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"F. Andersen and K. D. Petersen. Recursive Boolean Functions in HOL. In 1991 International Tutorial and Workshop on the HOL Theorem Proving System and its Applications, pages 367\u2013377. IEEE Computer Society, August 1991.","DOI":"10.1109\/HOL.1991.596301"},{"key":"1_CR5","unstructured":"R. Boulton. The HOL arith Library. Technical report, Computer Laboratory University of Cambridge, July 1992."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"A. Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 5, 1940.","DOI":"10.2307\/2266170"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"U. Engberg, P. Gr\u00f8nning, and L. Lamport. Mechanical Verification of Concurrent Systems with TLA. In Fourth International Workshop on Computer Aided Verification, 1992.","DOI":"10.1007\/3-540-56496-9_5"},{"key":"1_CR9","unstructured":"J. H. Gallier. Logic for Computer Science. Foundations of Automatic Theorem Proving. Harper & Row, Publishers, 1986."},{"key":"1_CR10","volume-title":"Technical report, DAIMI PB-258","author":"S. Garland","year":"1988","unstructured":"S. Garland, J. Guttag, and J. Staunstrup. Verification of VLSI circuits using LP. Technical report, DAIMI PB-258, University of \u00c5rhus, Denmark, July 1988."},{"issue":"9","key":"1_CR11","doi-asserted-by":"crossref","first-page":"1004","DOI":"10.1109\/32.58787","volume":"16","author":"D. M. Goldschlag","year":"1990","unstructured":"D. M. Goldschlag. Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover. IEEE Transactions on Software Engineering, 16(9):1004\u20131023, September 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon. HOL \u2014 A Proof Generating System for Higher-Order Logic. Cambridge University, Computer Laboratory, 1987.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"1_CR13","unstructured":"J. Harrison. The HOL reduce Library. Technical report, Computer Laboratory University of Cambridge, June 1991."},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"C.S. Jutla, E. Knapp, and J.R. Rao. A Predicate Transformer Approach to Semantics of Parallel Programs. ACM Symposium on Principles of Distributed Computing, 1989.","DOI":"10.1145\/72981.72999"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"T. Melham. Automating Recursive Type Definitions in Higher Order Logic. Technical Report No. 146, Computer Laboratory, University of Cambridge, Sept. 1988.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"S. Owicki and L. Lamport. Proving Liveness Properties of Concurrent Programs. ACM Transactions on Programming Languages and Systems, 4(3), July 1982.","DOI":"10.1145\/357172.357178"},{"key":"1_CR17","unstructured":"K. Schneider, R. Kumar, and T. Kropf. New Concepts in Faust. In 1992 International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 471\u2013493. imec Interuniversity Micro-Electronics Center, September 1992."},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"R. E. Shostak. Deciding Combinations of Theories. JACM, 31:1\u201312, 1984.","journal-title":"JACM"},{"issue":"2","key":"1_CR19","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF01898402","volume":"3","author":"B. A. Sanders","year":"1991","unstructured":"Beverly A. Sanders. Eliminating the Substitution Axiom from UNITY Logic. Formal Aspects of Computing, 3(2):189\u2013205, April\u2013June 1991.","journal-title":"Formal Aspects of Computing"},{"key":"1_CR20","unstructured":"K. Slind. HOL90 Users Manual. Technical report, 1992."},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"R. Smullyan. First Order Logic, volume 43 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, second printing 1971 edition, 1968.","DOI":"10.1007\/978-3-642-86718-7_4"}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57826-9_121.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:14:23Z","timestamp":1605647663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_121"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_121","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}