{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:06Z","timestamp":1725663666307},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540551799"},{"type":"electronic","value":"9783540467632"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55179-4_43","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T09:51:58Z","timestamp":1330249918000},"page":"466-476","source":"Crossref","is-referenced-by-count":3,"title":["Comparing generic state machines"],"prefix":"10.1007","author":[{"given":"M.","family":"Langevin","sequence":"first","affiliation":[]},{"given":"E.","family":"Cerny","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"M. R. Barbacci, \u201cA Comparison of Register Transfer Languages for Describing Computers and Digital Systems\u201d, IEEE Trans. on Comp., Vol. C-24, No. 2, February 1975.","key":"43_CR1","DOI":"10.1109\/T-C.1975.224181"},{"unstructured":"R. S. Boyer, J. S. Moore, \u201cA Computational Logic\u201d, ACM Monograph Series, Academic Press Inc., 1979.","key":"43_CR2"},{"doi-asserted-by":"crossref","unstructured":"R. E. Bryant, \u201cGraph-Based Algorithms for Boolean Function Manipulation\u201d, IEEE Trans. on Comp., Vol. C-35, No. 8, August 1986.","key":"43_CR3","DOI":"10.1109\/TC.1986.1676819"},{"doi-asserted-by":"crossref","unstructured":"B, Buchberger, R. Loos, \u201cAlgebraic Simplification\u201d, in Buchberger and al. eds., Computer Algebra: Symbolic and Algebraic Computation, Springer, 1982.","key":"43_CR4","DOI":"10.1007\/978-3-7091-3406-1_2"},{"doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang, \u201cSymbolic Model Checking: 1020 States and Beyond\u201d, in Proc. of the Int. Work. on Formal Methods in VLSI Design, Miami, January 1991.","key":"43_CR5","DOI":"10.1016\/0890-5401(92)90017-A"},{"volume-title":"Tautology Checking using Cross-Controllability and Cross-Observability Relations","year":"1990","author":"E. Cerny","unstructured":"E. Cerny, C. Mauras, \u201cTautology Checking using Cross-Controllability and Cross-Observability Relations\u201d, ICCAD, Santa Clara, November 1990.","key":"43_CR6"},{"doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, J. C. Madre, \u201cVerification of Synchronous Sequential Machines Using Symbolic Execution\u201d, in Proc. of the Work. on Automatic Verification Methods for Finite State Systems, Grenoble, June 1989.","key":"43_CR7","DOI":"10.1007\/3-540-52148-8_30"},{"unstructured":"O. Coudert, C. Berthet, J. C. Madre, \u201cVerification of Sequential Machines Using Boolean Functional Vectors\u201d, in L. Claesen, editor, Proc. of the int. Work. on Applied Formal Methods for Correct VLSI Design, Leuven, November 1989.","key":"43_CR8"},{"unstructured":"S. Devadas, H.-K. T. Ma, A. R. Newton, \u201cOn the Verification of Sequential Machines at Different Levels of Abstraction\u201d, IEEE Transaction on CAD, Vol. 6, No. 7, June 1988.","key":"43_CR9"},{"doi-asserted-by":"crossref","unstructured":"G. C. Gopalakrishnan, R. M. Fujimoto, V. Akella, N. S. Mani, \u201cHOP: A Process Model for Synchronous Hardware; Semantics and Experiments in Process Composition\u201d, Integration: The VLSI Journal, August 1989.","key":"43_CR10","DOI":"10.21236\/ADA203597"},{"unstructured":"M. Gordon, \u201cWhy Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware\u201d, in Formal Aspects of VLSI Design, 1986.","key":"43_CR11"},{"doi-asserted-by":"crossref","unstructured":"K. Knight, \u201cUnification: A Multidisciplinary Survey\u201d, ACM Computing Surveys, Vol. 21, No. 1, 1989.","key":"43_CR12","DOI":"10.1145\/62029.62030"},{"volume-title":"Switching and Finite Automata Theory","year":"1978","author":"S. Kohavi","unstructured":"S. Kohavi, \u201cSwitching and Finite Automata Theory\u201d, McGraw-Hill, New-York, 1978.","key":"43_CR13"},{"doi-asserted-by":"crossref","unstructured":"M. Langevin, \u201cAutomated RTL Verification Based on Predicate Calculus\u201d, in Proc. of the Work. on Computer Aided Verification, Rutgers, June 1990.","key":"43_CR14","DOI":"10.1090\/dimacs\/003\/36"},{"unstructured":"M. Langevin, E. Cerny, \u201cVerification of Processor-Like Circuit\u201d, in Proc. of the Advanced Research Workshop on Correct Hardware Design Methodologies, Turin, June 1991.","key":"43_CR15"},{"unstructured":"T. Larsson, \u201cHardware Verification Based on Algebraic Manipulation and Partial Evaluation\u201d, in Proc. of the Int. Working Conf. on the Fusion of Hardware Design and Verification, Glasgow, July 1988.","key":"43_CR16"},{"unstructured":"Z. Manna, \u201cMathematical Theory of Computation\u201d, McGraw-Hill, 1974.","key":"43_CR17"},{"unstructured":"L. Pierre, \u201cThe Formal Proof of the Min-Max Sequential Benchmark Described in CASCADE Using the Boyer-Moore Theorem Prover\u201d, in L. Claesen, editor, Proc. of the int. Work. on Applied Formal Methods for Correct VLSI Design, Leuven, November 1989.","key":"43_CR18"},{"unstructured":"C. Pixley, G. Beihl, \u201cQuotient and Isomorphism Theorems of a Theory of Sequential Hadrware Equivalence\u201d, in Proc. of the Int. Work. on Formal Methods in VLSI Design, Miami, January 1991.","key":"43_CR19"},{"volume-title":"Implicit State Enumeration of Finite State Machines Using BDDs","year":"1990","author":"H. J. Touati","unstructured":"H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, A. Sangiovanni-Vincentelli, \u201cImplicit State Enumeration of Finite State Machines Using BDDs\u201d, ICCAD, Santa Clara, November 1990.","key":"43_CR20"},{"unstructured":"VHDL Language Reference Manual, Intermetrics Inc., 1987.","key":"43_CR21"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55179-4_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T04:14:41Z","timestamp":1640924081000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55179-4_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540551799","9783540467632"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-55179-4_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}