{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:25:05Z","timestamp":1773098705506,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642363146","type":"print"},{"value":"9783642363153","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36315-3_15","type":"book-chapter","created":{"date-parts":[[2013,1,15]],"date-time":"2013-01-15T00:35:15Z","timestamp":1358210115000},"page":"183-196","source":"Crossref","is-referenced-by-count":13,"title":["Property Checking of Quantum Circuits Using Quantum Multiple-Valued Decision Diagrams"],"prefix":"10.1007","author":[{"given":"Julia","family":"Seiter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias","family":"Soeken","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Wille","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","volume-title":"Quantum Computation and Quantum Information","author":"M.A. Nielsen","year":"2000","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, New York (2000)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Hung, W.N.N., Song, X., Yang, G., Yang, J., Perkowski, M.A.: Quantum logic synthesis by symbolic reachability analysis. In: Malik, S., Fix, L., Kahng, A.B. (eds.) Design Automation Conference, pp. 838\u2013841. ACM (June 2004)","DOI":"10.1145\/996566.996790"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Shende, V.V., Bullock, S.S., Markov, I.L.: Synthesis of quantum logic circuits. In: Tang, T. (ed.) Asia and South Pacific Design Automation Conference, pp. 272\u2013275. ACM Press (January 2005)","DOI":"10.1145\/1120725.1120847"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Gro\u00dfe, D., Wille, R., Dueck, G.W., Drechsler, R.: Exact Synthesis of Elementary Quantum Gate Circuits for Reversible Functions with Don\u2019t Cares. In: Int\u2019l Symp. on Multiple-Valued Logic, pp. 214\u2013219 (May 2008)","DOI":"10.1109\/ISMVL.2008.42"},{"issue":"3","key":"15_CR5","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1109\/TCAD.2007.911334","volume":"27","author":"D. Maslov","year":"2008","unstructured":"Maslov, D., Dueck, G.W., Miller, D.M., Negrevergne, C.: Quantum Circuit Simplification and Level Compaction. IEEE Trans. on CAD\u00a027(3), 436\u2013444 (2008)","journal-title":"IEEE Trans. on CAD"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Dueck, G.W., Drechsler, R.: Window optimization of reversible and quantum circuits. In: Int\u2019l Symp. on Design and Diagnostics of Electronic Circuits and Systems, pp. 341\u2013345 (April 2010)","DOI":"10.1109\/DDECS.2010.5491754"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Yuan, J., Shultz, K., Pixley, C., Miller, H., Aziz, A.: Modeling design constraints and biasing in simulation using BDDs. In: Int\u2019l Conf. on Computer-Aided Design, pp. 584\u2013590 (November 1999)","DOI":"10.1109\/ICCAD.1999.810715"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Bergeron, J.: Writing Testbenches Using SystemVerilog. Springer (2006)","DOI":"10.1007\/0-387-31275-7"},{"key":"15_CR9","unstructured":"Yuan, J., Pixley, C., Aziz, A.: Constraint-Based Verification. Springer (January 2006)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Wille, R., Gro\u00dfe, D., Haedicke, F., Drechsler, R.: SMT-based Stimuli Generation in the SystemC Verification Library. In: Forum on Specification & Design Languages (September 2009)","DOI":"10.1007\/978-90-481-9304-2_14"},{"key":"15_CR11","unstructured":"Brand, D.: Verification of large synthesized designs. In: Lightner, M.R., Jess, J.A.G. (eds.) Int\u2019l Conf. on Computer-Aided Design, pp. 534\u2013537. IEEE Computer Society (1993)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Disch, S., Scholl, C.: Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets. In: Asia and South Pacific Design Automation Conference, pp. 938\u2013943 (2007)","DOI":"10.1109\/ASPDAC.2007.358110"},{"key":"15_CR13","volume-title":"Model Checking","author":"E.M. Clarke Jr.","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Miller, D.M., Thornton, M.A.: QMDD: A Decision Diagram Structure for Reversible and Quantum Circuits. In: Int\u2019l Symp. on Multiple-Valued Logic, p.\u00a030. IEEE Computer Society (May 2006)","DOI":"10.1109\/ISMVL.2006.35"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058, 117\u2013148 (2003)","journal-title":"Advances in Computers"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Wille, R., Gro\u00dfe, D., Miller, D.M., Drechsler, R.: Equivalence Checking of Reversible Circuits. In: Int\u2019l Symp. on Multiple-Valued Logic, pp. 324\u2013330. IEEE Computer Society (May 2009)","DOI":"10.1109\/ISMVL.2009.19"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-540-70545-1_51","volume-title":"Computer Aided Verification","author":"S.J. Gay","year":"2008","unstructured":"Gay, S.J., Nagarajan, R., Papanikolaou, N.: QMC: A Model Checker for Quantum Systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 543\u2013547. Springer, Heidelberg (2008)"},{"key":"15_CR19","doi-asserted-by":"publisher","first-page":"52328","DOI":"10.1103\/PhysRevA.70.052328","volume":"70","author":"S. Aaronson","year":"2004","unstructured":"Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Phys. Rev. A\u00a070, 052328 (2004)","journal-title":"Phys. Rev. A"},{"key":"15_CR20","doi-asserted-by":"publisher","first-page":"147902","DOI":"10.1103\/PhysRevLett.91.147902","volume":"91","author":"G. Vidal","year":"2003","unstructured":"Vidal, G.: Efficient Classical Simulation of Slightly Entangled Quantum Computations. Phys. Rev. Letters\u00a091, 147902 (2003)","journal-title":"Phys. Rev. Letters"},{"key":"15_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-3065-8","volume-title":"Quantum Circuit Simulation","author":"G.F. Viamontes","year":"2009","unstructured":"Viamontes, G.F., Markov, I.L., Hayes, J.P.: Quantum Circuit Simulation. Springer, Heidelberg (2009)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Deutsch, D.: Quantum Theory, the Church-Turing Principle and the Universal Quantum Computer. Royal Society London A 400(1818) (July 1985)","DOI":"10.1098\/rspa.1985.0070"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Miller, D.M., Wille, R., Dueck, G.: Synthesizing Reversible Circuits for Irreversible Functions. In: EUROMICRO Symp. on Digital System Design, pp. 749\u2013756 (2009)","DOI":"10.1109\/DSD.2009.186"}],"container-title":["Lecture Notes in Computer Science","Reversible Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36315-3_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T17:08:34Z","timestamp":1745946514000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36315-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642363146","9783642363153"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36315-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}