{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:19:46Z","timestamp":1742617186240,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581796"},{"type":"electronic","value":"9783540484691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_59","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:25:05Z","timestamp":1330269905000},"page":"247-259","source":"Crossref","is-referenced-by-count":17,"title":["Ground temporal logic: A logic for hardware verification"],"prefix":"10.1007","author":[{"given":"David","family":"Cyrluk","sequence":"first","affiliation":[]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi and Leslie Lamport. The existence of refinement mappings. In Third Annual Symposium on Logic in Computer Science, pages 165\u2013175. IEEE, Computer Society Press, July 1988.","DOI":"10.1109\/LICS.1988.5115"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, D. L. Beatty, and C.-J. Seger. Formal hardware verification by symbolic trajectory evaluation. In 28th ACM\/IEEE Design Automation Conference, 1991.","DOI":"10.1145\/127601.127701"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM\/IEEE Design Automation Conference, 1990.","DOI":"10.1145\/123186.123223"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E.M. Clarke, and D.E. Long. Representing circuits more efficiently in symbolic model checking. In 28th ACM\/IEEE Design Automation Conference, 1991.","DOI":"10.1145\/127601.127702"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"J. R. Burch and D. L. Dill. Automated verification of pipelined microprocessor control. In CAV '94, 1994. Submitted.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Nineteenth Annual ACM Symposium on Principles of Programming Languages, pages 343\u2013354, 1992.","DOI":"10.1145\/143165.143235"},{"key":"21_CR8","unstructured":"W Cullyer and C Pygott. Hardware proofs using LCF-LSM and ELLA. Memorandum 3832, RSRE, September 1985."},{"key":"21_CR9","unstructured":"D. Cyrluk and P. Narendran. Decision problems for ground temporal logics. Unpublished Manuscript."},{"key":"21_CR10","unstructured":"David Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, SRI Computer Science Laboratory, December 1993."},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"T. Henzinger. Half-order modal logic: How to prove real-time properties. In Proceedings of the Ninth Annual Symposium on Principles of Distributed Computing, pages 281\u2013296. ACM Press, 1990.","DOI":"10.1145\/93385.93429"},{"key":"21_CR12","unstructured":"W.A. Hunt. The mechanical verification of a microprocessor design. In Proc. of IFIP Working Conference on From H.D.L Descriptions to Guaranteed Correct Circuit Designs, 1986."},{"key":"21_CR13","unstructured":"J. Joyce, G. Birtwistle, and M. Gordon. Proving a computer correct in higher order logic. Technical Report 100, Computer Lab., University of Cambridge, 1986."},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Fred Kr\u00f6ger. Temporal Logic of Programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer Verlag, 1987.","DOI":"10.1007\/978-3-642-71549-5_5"},{"key":"21_CR15","volume-title":"Technical Report 79","author":"L. Lamport","year":"1991","unstructured":"Leslie Lamport. The temporal logic of actions. Technical Report 79, Digital Systems Research Center, Palo Alto, California 94301, December 1991."},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Paul Loewenstein and David Dill. Verification of multiprocessor cache protocol using simulation relations and higher-order logic. In Computer-Aided Verification '90, pages 187\u2013205. DIMACS, American Mathematical Society, 1991.","DOI":"10.1090\/dimacs\/003\/14"},{"key":"21_CR17","first-page":"163","volume-title":"Foundations of Computer Science IV, Distributed Systems: Part 2, Mathematical Centre Tracts 159","author":"Z. Manna","year":"1983","unstructured":"Z. Manna and A. Pnueli. Verification of concurrent programs: A temporal proof system. In J. W. de Bakker annd J. van Leeuwen, editor, Foundations of Computer Science IV, Distributed Systems: Part 2, Mathematical Centre Tracts 159, pages 163\u2013255. Center for Mathematics and Computer Science, Amsterdam, 1983."},{"issue":"2","key":"21_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, October 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Sam Owre, John M. Rushby, and Natarajan Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, Automated Deduction \u2014 CADE-11, 11th International Conference on Automated Deduction, Lecture Notes in Artifical Intelligence, pages 748\u2013752. Springer Verlag, June 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"21_CR20","volume-title":"Technical Report 78","author":"J. B. Saxe","year":"1991","unstructured":"James B. Saxe, Stephen J. Garland, John V. Guttag, and James J. Horning. Using transformations and verification in circuit design. Technical Report 78, Digital Systems Research Center, Palo Alto, California 94301, September 1991."},{"issue":"5","key":"21_CR21","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"Mandayam Srivas and Mark Bickford. Formal verification of a pipelined microprocessor. IEEE Software, 7(5):52\u201364, September 1990.","journal-title":"IEEE Software"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_59.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:21:31Z","timestamp":1742595691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_59"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_59","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}