{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:40:55Z","timestamp":1725493255932},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651918"},{"type":"electronic","value":"9783540495192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_25","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T06:37:12Z","timestamp":1192862232000},"page":"387-402","source":"Crossref","is-referenced-by-count":4,"title":["Formally Verifying Data and Control with Weak Reachability Invariants"],"prefix":"10.1007","author":[{"given":"Jeffrey","family":"Su","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens U.","family":"Skakkeb\u00c6k","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"25_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification (CAV)98","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally and automatically. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification (CAV)98, volume 1427 of Lecture Notes in Computer Science, pages 319\u2013331, Vancouver, BC, Canada, June\/July 1998. Springer-Verlag."},{"key":"25_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-61474-5_80","volume-title":"Computer Aided Verification (CAV)96","author":"S. Bensalem","year":"1996","unstructured":"Saddek Bensalem, Yassine Lakhnech, and Hassen Sa\u00cfdi. Powerful techniques for the automatic generation of invariants. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification (CAV)96, volume 1102 of Lecture Notes in Computer Science, pages 323\u2013335, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"issue":"1","key":"25_CR3","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N. S. Bj\u00d8rner","year":"1997","unstructured":"N. S. Bj\u00d8rner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1):49\u201387, February 1997.","journal-title":"Theoretical Computer Science"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"R. E. Bryant, D. L. Beatty, and C.-J. H. Seger. Formal hardware verification by symbolic ternary trajectory evaluation. In 28th ACM\/IEEE Design Automation Conference, 1991.","DOI":"10.1145\/127601.127701"},{"key":"25_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":"25_CR6","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":"25_CR7","doi-asserted-by":"crossref","unstructured":"M. Caplain. Finding invariant assertions for proving programs. In International Conference on Reliable Software, pages 165\u2013171, 1975.","DOI":"10.1145\/800027.808436"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"W. Carter, W. Joyner, and D. Brand. Symbolic simulation for correct machine design. In 16th Design Automation Conference Proceedings (1979), pages 280\u2013286, June 1979.","DOI":"10.1109\/DAC.1979.1600119"},{"key":"25_CR9","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"R. Floyd","year":"1967","unstructured":"R. Floyd. Assigning meaning to programs. In Proc. Symposium in Applied Mathematics, volume 19, pages 19\u201332, 1967.","journal-title":"Proc. Symposium in Applied Mathematics"},{"key":"25_CR10","volume-title":"The Language of machines: an introduction to computability and formal languages","author":"R. W. Floyd","year":"1994","unstructured":"R. W. Floyd. The Language of machines: an introduction to computability and formal languages. New York: Computer Science Press, 1994."},{"issue":"1","key":"25_CR11","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1109\/TSE.1975.6312821","volume":"1","author":"S. German","year":"1975","unstructured":"S. German and B. Wegbreit. A synthesizer of inductive assertions. IEEE Transactions on Software Enginnering, 1(1):68\u201375, March 1975.","journal-title":"IEEE Transactions on Software Enginnering"},{"key":"25_CR12","unstructured":"G. Kane. MIPS RISC Architecture. Prentice Hall, 1988."},{"key":"25_CR13","unstructured":"S. Katz and Z. Manna. A heuristic approach to program verification. In Proceedings: 3rd International Joint Conference on Artificial Intelligence, pages 500\u2013512, 1976."},{"key":"25_CR14","first-page":"234","volume":"1","author":"J. King","year":"1972","unstructured":"J King. A program verifier. In Information Processing 71 Proceedings of the IFIP Congress, volume 1, pages 234\u2013249, 1972.","journal-title":"Information Processing 71 Proceedings of the IFIP Congress"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"B. Levy. Microcode verification using sdvs-the method and a case study. In 17th MICRO(1984), pages 234\u2013245, 1984.","DOI":"10.21236\/ADA175253"},{"issue":"4","key":"25_CR16","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/MS.1986.233753","volume":"3","author":"R. Mueller","year":"1986","unstructured":"R. Mueller and M. Ruda. Formal methods of microcode verification and synthesis. IEEE Software, 3(4):38\u201348, July 1986.","journal-title":"IEEE Software"},{"issue":"2","key":"25_CR17","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. E. Nelson","year":"1979","unstructured":"G. E. 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":"25_CR18","series-title":"Lect Notes Comput Sci","first-page":"72","volume-title":"Computer Aided Verification (CAV)97","author":"H. Sa\u00cfdi","year":"1997","unstructured":"Hassen Sa\u00cfdi and Susanne Graf. Construction of abstract state graphs with PVS. In Orna Grumberg, editor, Computer Aided Verification (CAV)97, volume 1254 of Lecture Notes in Computer Science, pages 72\u201383, Haifa, Israel, June 1997. Springer-Verlag."},{"issue":"2","key":"25_CR19","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R. E. Shostak","year":"1979","unstructured":"R. E. Shostak. A practical decision procedure for arithmetic with function symbols. Journal of the ACM, 26(2):351\u2013360, April 1979.","journal-title":"Journal of the ACM"},{"key":"25_CR20","unstructured":"R. E. Shostak. Deciding combinations of theories. Technical Report SRI-CSL-132, Computer Science Laboratory, SRI International, February 1982."},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"M. Smith, M. Horowitz, and M. Lam. Efficient superscalar performance through boosting. In 5th International Conference on Architectural Support for Programming languages and Operating Systems, pages 248\u2013259, Boston, MA, 1992. IEEE\/ACM.","DOI":"10.1145\/143365.143534"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"M. Smith, M. Lam, and M. Horowitz. Boosting beyond static scheduling in a superscalar processor. In 17th International Symposium on Computer Architecture, volume 18-2, pages 344\u2013354, Seattle, WA, May 1990. IEEE\/ACM.","DOI":"10.1145\/325096.325160"},{"key":"25_CR23","unstructured":"J. Su, L. Arditi, S. Das, J. U. Skakkeb\u00c6k, and D. L. Dill. Formal verification of the TORCH microprocessor RTL design. Unpublished, 1998."},{"key":"25_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/BFb0031822","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"J. X. Su","year":"1996","unstructured":"Jeffrey X. Su, David L. Dill, and Clark W. Barrett. Automatic generation of invariants in processor verification. In M. Srivas and A. Camilleri, editors, Formal Methods in Computer Aided Design (FMCAD), volume 1166 of Lecture Notes in Computer Science, pages 197\u2013201. Springer-Verlag, November 1996."},{"issue":"3","key":"25_CR25","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1145\/322261.322272","volume":"28","author":"R. Tarjan","year":"1981","unstructured":"R. Tarjan. A unify approach to path problems. Journal of the ACM, 28(3):577\u2013593, July 1981.","journal-title":"Journal of the ACM"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Z. Zhou, X. Song, S. Tahar, E. Cerny, F. Corella, and M. Langevin. Formal verification of the island tunnel controller using multiway decision graphs. In M. Srivas and A. Camilleri, editors, Formal Methods in Computer Aided Design (FMCAD), volume 1166, pages 233\u2013247. Springer-Verlag, November 1996.","DOI":"10.1007\/BFb0031811"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49519-3_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T17:59:16Z","timestamp":1556906356000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}