{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T12:08:39Z","timestamp":1772021319541,"version":"3.50.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1992,7,1]],"date-time":"1992-07-01T00:00:00Z","timestamp":709948800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1992,7]]},"DOI":"10.1007\/bf00464357","type":"journal-article","created":{"date-parts":[[2004,11,14]],"date-time":"2004-11-14T13:09:30Z","timestamp":1100437770000},"page":"61-115","source":"Crossref","is-referenced-by-count":36,"title":["Probabilistic verification of Boolean functions"],"prefix":"10.1007","volume":"1","author":[{"given":"Jawahar","family":"Jain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacob A.","family":"Abraham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Bitner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Donald S.","family":"Fussell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"27","author":"S.B. Akers","year":"1978","unstructured":"S.B.Akers. Binary decision diagrams. IEEE Transactions on Computers, C-27:509?516 (June 1978).","journal-title":"IEEE Transactions on Computers"},{"key":"CR2","unstructured":"C.L. Berman. Circuit width, register allocation, and reduced function graphs. IBM Research Report, RC 14129 (October 1988)."},{"key":"CR3","unstructured":"C.L. Berman and L. Trevillyan. Functional comparison of logic designs for VLSI chips. IBM Research Report, RC 14137 (October 1988)."},{"key":"CR4","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1016\/S0020-0190(80)90078-2","volume":"10","author":"M. Blum","year":"1980","unstructured":"M.Blum, A.K.Chandra, and M.N.Wegman. Equivalence of free Boolean graphs can be decided probabilistically in polynomial time. Information Processing Letters, 10:80?82 (March 1980).","journal-title":"Information Processing Letters"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"K.S. Brace, R.L. Rudell, and R.E. Bryant. Efficient implementation of a BDD package. 27th Design Automation Conference, pp. 40?45.","DOI":"10.1145\/123186.123222"},{"key":"CR6","unstructured":"F. Brglez and H. Fujiwara. A neutral netlist of 10 combinational benchmark circuits and a target translator in FORTRAN. IEEE International Symposium on Circuits and Systems, June 1985, pp. 695?698."},{"key":"CR7","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E.Bryant. Graph based algorithms for Boolean function representation. IEEE Transactions on Computers, C-35:677?690 (August 1986).","journal-title":"IEEE Transactions on Computers"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1109\/12.73590","volume":"40","author":"R.E. Bryant","year":"1991","unstructured":"R.E.Bryant. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Transactions on Computers, C-40:206?213 (February 1991).","journal-title":"IEEE Transactions on Computers"},{"key":"CR9","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. 27th Design Automation Conference, 1990, pp. 46?51.","DOI":"10.1145\/123186.123223"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/2.65","volume":"21","author":"P. Camurati","year":"1988","unstructured":"P.Camurati and P.Prinetto. Formal verification of hardware correctness: Introduction and survey of current procedure. IEEE Computer, 21:8?19 (July 1988).","journal-title":"IEEE Computer"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"E. Cerny and C. Mauras. Tautology checking using cross-controllability and cross-observability relations. ICCAD, 1990 pp. 34?37.","DOI":"10.1109\/ICCAD.1990.129833"},{"key":"CR12","first-page":"227","volume-title":"Lecture Notes in Computer Science","author":"L. Fortune","year":"1978","unstructured":"L.Fortune, J.Hopcroft, and E.M.Schmidt. The complexity of equivalence and containment for free single variable program schemes. Lecture Notes in Computer Science 62: 227?240, Goos, Hartmanis, Ausiello, and Baum (eds.), Springer-Verlag, New York, 1978."},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"M. Fujita, H. Fujisawa, and N. Kawato. Evaluation and improvements of Boolean comparison method based on binary decision diagrams. ICCAD, 1988, pp. 2?5.","DOI":"10.1109\/ICCAD.1988.122450"},{"key":"CR14","unstructured":"J. Jain, J. Bitner, J. Abraham, and D. Fussell. Functional partitioning for verification and related problems. Brown\/MIT VLSI Conference, March 1992, pp. 210?226."},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"S.W. Jeong, B. Plessier, G. Hachtel, and F. Somenzi. Extended BDDs: Trading off canonicity for structure in verification algorithms. ICCAD, 1991, pp. 464?467.","DOI":"10.1109\/ICCAD.1991.185305"},{"key":"CR16","unstructured":"R. Kapur. Personal communication, September 1991."},{"key":"CR17","unstructured":"K. Karplus. Using if-then-else dag's for multi-level minimization. Decennial Caltech Conference on VLSI, May 1989."},{"key":"CR18","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C.Y. Lee","year":"1959","unstructured":"C.Y.Lee. Representation of switching circuits by binary-decision programs. Bell Systems Technology Journal, 38:985?999 (1959).","journal-title":"Bell Systems Technology Journal"},{"key":"CR19","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1145\/357062.357071","volume":"1","author":"T. Lengauer","year":"1979","unstructured":"T.Lengauer and R.Tarjan. A fast algorithm for finding dominators in a flowgraph. ACM Transactions on Programming Languages, 1:121?141 (July 1979).","journal-title":"ACM Transactions on Programming Languages"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"J.C. Madre and J.P. Billon. Proving circuit correctness using formal comparison between expected and extracted behavior. 25th Design Automation Conference, 1988, pp. 205?210.","DOI":"10.1109\/DAC.1988.14759"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"S. Malik, A. Wang, R.K. Brayton, and A. Sangiovanni-Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. ICCAD, 1988, pp. 6?9.","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"CR22","doi-asserted-by":"crossref","first-page":"593","DOI":"10.1145\/356893.356898","volume":"14","author":"B.M.E. Moret","year":"1982","unstructured":"B.M.E.Moret. Decision trees and diagrams. Computing Surveys, 14:593?623 (December 1982).","journal-title":"Computing Surveys"},{"key":"CR23","doi-asserted-by":"crossref","first-page":"668","DOI":"10.1109\/T-C.1975.224279","volume":"24","author":"K.P. Parker","year":"1975","unstructured":"K.P.Parker and E.J.McCluskey. Correspondence: Probabilistic treatment of general combinational networks. IEEE Transactions on Computer, C-24:668?670 (June 1975).","journal-title":"IEEE Transactions on Computer"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1099\/00221287-98-2-595","volume":"98","author":"R.W. Payne","year":"1977","unstructured":"R.W.Payne. Reticulation and other methods for reducing the size of printed diagnostic keys. Journal of General Microbiology, 98:595?597 (1977).","journal-title":"Journal of General Microbiology"},{"key":"CR25","unstructured":"D.E. Ross. Personal communication, March 1991."},{"key":"CR26","first-page":"423","volume":"1","author":"D.E. Rumelhart","year":"1986","unstructured":"D.E.Rumelhart, J.L.McClelland, et. al. Parallel distributed processing. The MIT Press, 1:423?443 (1986).","journal-title":"The MIT Press"},{"key":"CR27","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1145\/322261.322268","volume":"28","author":"S.K. Kumar","year":"1981","unstructured":"S.K.Kumar and M.A.Breuer. Probabilistic aspects of Boolean switching functions via a new transform. Journal of ACM, 28:502?520 (July 1981).","journal-title":"Journal of ACM"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00464357.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00464357\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00464357","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,20]],"date-time":"2024-12-20T01:33:25Z","timestamp":1734658405000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00464357"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,7]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,7]]}},"alternative-id":["BF00464357"],"URL":"https:\/\/doi.org\/10.1007\/bf00464357","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,7]]}}}