{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T15:22:29Z","timestamp":1729610549789,"version":"3.28.0"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,5]]},"DOI":"10.1109\/snpd.2016.7515871","type":"proceedings-article","created":{"date-parts":[[2016,7,26]],"date-time":"2016-07-26T20:38:58Z","timestamp":1469565538000},"page":"13-18","source":"Crossref","is-referenced-by-count":1,"title":["Automatic verification of non-recursive algorithm of Hanoi Tower by using Isabelle Theorem Prover"],"prefix":"10.1109","author":[{"given":"Huazhen","family":"Xu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhen","family":"You","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jinyun","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"doi-asserted-by":"publisher","key":"ref10","DOI":"10.1007\/BFb0059696"},{"year":"1976","author":"dijkstra","article-title":"A Discipline of Programming","key":"ref11"},{"year":"1989","author":"dijkstra","article-title":"Predicate Calculus and Program Semantics","key":"ref12"},{"key":"ref13","first-page":"748","article-title":"PVS: A prototype verification system","author":"sam","year":"1992","journal-title":"Automated Deduction—CADE-11"},{"year":"2001","author":"owre","journal-title":"PVS Language Reference Version 2 3","key":"ref14"},{"key":"ref15","article-title":"PVS: Combining specification, proof checking, and model checking","author":"sam","year":"1996","journal-title":"Computer Aided Verification"},{"key":"ref16","article-title":"An executable formalization of the HOL\/Nuprl connection in the metalogical framework Twelf","author":"nipkow","year":"2006","journal-title":"Logic for Programming Artificial Intelligence and Reasoning"},{"year":"2015","author":"bickford","journal-title":"Nuprl's Inductive Logical Forms[J]","key":"ref17"},{"key":"ref18","volume":"4","author":"matt","year":"2013","journal-title":"Computer-Aided Reasoning ACL2 Case Studies"},{"year":"2006","author":"matt","article-title":"ACL2 homepage","key":"ref19"},{"key":"ref4","first-page":"241","article-title":"Research on Tower of Hanoi non recursive algorithm[J]","volume":"5","author":"dongyue","year":"2008","journal-title":"Computer Applications and Software"},{"key":"ref27","first-page":"85","article-title":"Formal verification of algorithm program based on the Isabelle theorem prover[J]","volume":"10","author":"zhen","year":"2009","journal-title":"Computer Engineering and Science"},{"key":"ref3","first-page":"375","article-title":"A new non recursive solution of Hanoi Tower problem [J]","volume":"4","author":"xiaobing","year":"2004","journal-title":"Journal of China Three Gorges University (NATURAL SCIENCE EDITION)"},{"key":"ref6","first-page":"48","article-title":"The exploration and research of Hanoi algorithm[J]","volume":"7","author":"yunxia","year":"2013","journal-title":"Internet of Things Technology"},{"key":"ref5","first-page":"96","article-title":"Non recursive algorithm about four tower of Hanoi[J]","volume":"11","author":"jun","year":"2013","journal-title":"Fujian Computer"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meanings to programs, in Mathematical Aspects of Computer Science","volume":"19","author":"floyd","year":"1967","journal-title":"Proc of a Symposium in Applied Mathematics"},{"key":"ref7","first-page":"10","article-title":"Tower of Hanoi non recursive algorithm [J]","volume":"14","author":"wen","year":"2009","journal-title":"Computer Programming Skills and Maintenance"},{"key":"ref2","first-page":"143","article-title":"The formal derivation of Hanoi Tower nonrecursive algorithm and correctness verification","volume":"s1","author":"zhen","year":"2008","journal-title":"Journal of Computer research and development"},{"key":"ref9","first-page":"322","article-title":"An axiomatic approach to computer programming Comm ACM","volume":"12","author":"hoare","year":"1969"},{"year":"0","key":"ref1"},{"key":"ref20","article-title":"Interpretation of locales in Isabelle: Theories and proof contexts","author":"clemens","year":"2006","journal-title":"Mathematical Knowledge Management"},{"key":"ref22","first-page":"279","article-title":"IsaPlanner: A prototype proof planner in Isabelle","author":"lucas","year":"2003","journal-title":"Automated Deduction - CADE-20"},{"year":"2015","author":"nipkow","article-title":"Programming and Proving in Isabelle\/HOL","key":"ref21"},{"key":"ref24","first-page":"12","article-title":"Automatic proof and disproof in Isabelle\/HOL","author":"jasmin","year":"2011","journal-title":"Frontiers of Combining Systems"},{"year":"2015","author":"tobias","article-title":"A Proof Assistant for Higher-Order Logic","key":"ref23"},{"key":"ref26","article-title":"PAR method Abstract Programming Language Apla technical report","volume":"9","author":"jinyun","year":"2001","journal-title":"Key Laboratory of high performance computing technology Jiangxi Normal University"},{"doi-asserted-by":"publisher","key":"ref25","DOI":"10.1007\/BF02939477"}],"event":{"name":"2016 17th IEEE\/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel\/Distributed Computing (SNPD)","start":{"date-parts":[[2016,5,30]]},"location":"Shanghai, China","end":{"date-parts":[[2016,6,1]]}},"container-title":["2016 17th IEEE\/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel\/Distributed Computing (SNPD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7510515\/7515861\/07515871.pdf?arnumber=7515871","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T19:15:13Z","timestamp":1498331713000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7515871\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/snpd.2016.7515871","relation":{},"subject":[],"published":{"date-parts":[[2016,5]]}}}