{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:04:26Z","timestamp":1746745466867},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540283720"},{"type":"electronic","value":"9783540318200"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11541868_17","type":"book-chapter","created":{"date-parts":[[2010,7,20]],"date-time":"2010-07-20T19:12:52Z","timestamp":1279653172000},"page":"261-277","source":"Crossref","is-referenced-by-count":7,"title":["Verification of BDD Normalization"],"prefix":"10.1007","author":[{"given":"Veronika","family":"Ortner","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Schirmer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R. Bornat","year":"2000","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000, vol.\u00a01837, pp. 102\u2013126. Springer, Heidelberg (2000)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: Proceedings. 27th ACM\/IEEE. Design Automation Conference, June 1990, pp. 40\u201345 (1990)","DOI":"10.1145\/123186.123222"},{"issue":"8","key":"17_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"17_CR4","unstructured":"Burstall, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 7, pp. 23\u201350. Edinburgh University Press (1972)"},{"key":"17_CR5","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-47813-2_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Krstic","year":"2002","unstructured":"Krstic, S., Matthews, J.: Verifying BDD algorithms through monadic interpretation. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 182\u2013195. Springer, Heidelberg (2002)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-45085-6_10","volume-title":"Automated Deduction \u2013 CADE-19","author":"F. Mehta","year":"2003","unstructured":"Mehta, F., Nipkow, T.: Proving Pointer Programs in Higher-Order Logic. In: Baader, F. (ed.) CADE 2003. LNCS, vol.\u00a02741, pp. 121\u2013135. Springer, Heidelberg (2003)"},{"key":"17_CR9","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/3-540-39185-1_15","volume-title":"Types for Proofs and Programs","author":"T. Nipkow","year":"2003","unstructured":"Nipkow, T.: Structured proofs in isar\/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002, vol.\u00a02646, pp. 259\u2013278. Springer, Heidelberg (2003), \n                    \n                      http:\/\/isabelle.in.tum.de\/docs.html"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer-Verlag, Heidelberg (2002), \n                    \n                      http:\/\/www.in.tum.de\/~nipkow\/LNCS2283\/"},{"key":"17_CR11","unstructured":"Ortner, V.: Verification of BDD Algorithms. Master\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen (2004), available from \n                    \n                      http:\/\/www.veronika.langlotz.info\/"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-32275-7_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N. Schirmer","year":"2005","unstructured":"Schirmer, N.: A verification environment for sequential imperative programs in Isabelle\/HOL. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 398\u2013414. Springer, Heidelberg (2005)"},{"key":"17_CR14","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-44464-5_13","volume-title":"Advances in Computing Science - ASIAN 2000","author":"K.N. Verma","year":"2000","unstructured":"Verma, K.N., Goubault-Larrecq, J., Prasad, S., Arun-Kumar, S.: Reflecting BDDs in Coq. In: He, J., Sato, M. (eds.) ASIAN 2000, vol.\u00a01961, pp. 162\u2013181. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11541868_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:56:30Z","timestamp":1619506590000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11541868_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283720","9783540318200"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/11541868_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}