{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:51:04Z","timestamp":1742957464205,"version":"3.40.3"},"publisher-location":"Wiesbaden","reference-count":58,"publisher":"Springer Fachmedien Wiesbaden","isbn-type":[{"type":"print","value":"9783658099930"},{"type":"electronic","value":"9783658099947"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-658-09994-7_5","type":"book-chapter","created":{"date-parts":[[2015,6,5]],"date-time":"2015-06-05T07:56:17Z","timestamp":1433490977000},"page":"122-150","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Modeling Unknown Values in Test and Verification"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Becker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Sauer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Wimmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,6]]},"reference":[{"issue":"4","key":"5_CR1","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1147\/rd.104.0278","volume":"10","author":"J.P. Roth","year":"1966","unstructured":"Roth, J.P.: Diagnosis of automata failures: A calculus and a method. IBM J. Res. Dev. 10(4) (1966) 278\u2013291","journal-title":"IBM J. Res. Dev"},{"unstructured":"Goel, P.: An implicit enumeration algorithm to generate tests for combinational logic circuits. In: Proc. Fault Tolerant Computing Symposium. (1980) 145\u2013151","key":"5_CR2"},{"doi-asserted-by":"crossref","unstructured":"Fujiwara, H., Shimono, T.: On the acceleration of test generation algorithms. IEEE Trans. on Computers C-32(12) (1983) 1137 -1144","key":"5_CR3","DOI":"10.1109\/TC.1983.1676174"},{"issue":"1","key":"5_CR4","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T. Larrabee","year":"1992","unstructured":"Larrabee, T.: Test pattern generation using Boolean satisfiability. IEEE Trans. on Computer-Aided Design 11(1) (1992) 4\u201315","journal-title":"IEEE Trans. on Computer-Aided Design"},{"issue":"9","key":"5_CR5","doi-asserted-by":"publisher","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"P. Stephan","year":"1996","unstructured":"Stephan, P., Brayton, R., Sangiovanni-Vincentelli, A.: Combinational test generation using satisfiability. IEEE Trans. on CAD of Integrated Circuits and Systems 15(9) (1996) 1167\u20131176","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"issue":"3\u20134","key":"5_CR6","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10766-009-0124-7","volume":"38","author":"A. Czutro","year":"2010","unstructured":"Czutro, A., Polian, I., Lewis, M., Engelke, P., Reddy, S.M., Becker, B.: Thread- parallel integrated test pattern generator utilizing satisfiability analysis. International Journal of Parallel Programming 38(3\u20134) (2010) 185\u2013202","journal-title":"International Journal of Parallel Programming"},{"doi-asserted-by":"crossref","unstructured":"Eggersgl\u00fc\u00df, S., Drechsler, R.: Atpg based on Boolean satisfiability. In: High Quality Test Pattern Generation and Boolean Satisfiability. Springer (2012) 59\u201370","key":"5_CR7","DOI":"10.1007\/978-1-4419-9976-4_4"},{"doi-asserted-by":"crossref","unstructured":"Wohl, P., Waicukauski, J., Neuveux, F.: Increasing scan compression by using X-chains. In: Int\u2019l Test Conference (ITC). (2008) 1\u201310","key":"5_CR8","DOI":"10.1109\/TEST.2008.4700646"},{"doi-asserted-by":"crossref","unstructured":"Ramdas, A., Sinanoglu, O.: Toggle-masking scheme for X-filtering. In: European Test Symposium (ETS). (2012) 1\u20136","key":"5_CR9","DOI":"10.1109\/ETS.2012.6233024"},{"issue":"10","key":"5_CR10","doi-asserted-by":"publisher","first-page":"1573","DOI":"10.1109\/TCAD.2009.2028679","volume":"28","author":"N. Ahmed","year":"2009","unstructured":"Ahmed, N., Tehranipoor, M.: A novel faster-than-at-speed transition-delay test method considering IR-drop effects. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 28(10) (2009) 1573\u20131582","journal-title":"IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems"},{"doi-asserted-by":"crossref","unstructured":"Hillebrecht, S., Polian, I., Engelke, P., Becker, B., Keim, M., Cheng, W.T.: Extraction, simulation and test generation for interconnect open defects based on enhanced aggressor-victim model. In: Int\u2019l Test Conference (ITC). (2008) 1\u201310","key":"5_CR11","DOI":"10.1109\/TEST.2008.4700642"},{"doi-asserted-by":"crossref","unstructured":"Muth, P.: A nine-valued circuit model for test generation. IEEE Trans. on Computers C-25(6) (1976) 630\u2013636","key":"5_CR12","DOI":"10.1109\/TC.1976.1674663"},{"unstructured":"Flores, P., Neto, H., Marques Silva, J.: An exact solution to the minimum size test pattern problem. In: IEEE Int\u2019l Conf. on Computer Design (ICCD). (1998) 510\u2013515","key":"5_CR13"},{"unstructured":"Jain, A., Boppana, V., Mukherjee, R., Jain, J., Fujita, M., Hsiao, M.: Testing, verification, and diagnosis in the presence of unknowns. In: IEEE VLSI Test Symposium (VTS). (2000) 263\u2013268","key":"5_CR14"},{"unstructured":"Carter, J., Rosen, B., Smith, G., Pitchumani, V.: Restricted symbolic evaluation is fast and useful. In: IEEE\/ACM Int\u2019l Conf. on Computer Aided Design (ICCAD). (1989) 38 -41","key":"5_CR15"},{"unstructured":"Kundu, S., Nair, I., Huisman, L., Iyengar, V.: Symbolic implication in test generation. In: Proc. Conference on European Design Automation. (1991) 492\u2013496","key":"5_CR16"},{"doi-asserted-by":"crossref","unstructured":"Touba, N.: X-canceling MISR : An X-tolerant methodology for compacting output responses with unknowns using a MISR. In: Int\u2019l Test Conference (ITC). (2007) 1\u201310","key":"5_CR17","DOI":"10.1109\/TEST.2007.4437576"},{"issue":"2","key":"5_CR18","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1109\/TVLSI.2005.863742","volume":"14","author":"Y. Tang","year":"2006","unstructured":"Tang, Y., Wunderlich, H., Engelke, P., Polian, I., Becker, B., Schloffel, J., Hapke, F., Wittke, M.: X-masking during logic BIST and its impact on defect coverage. IEEE Trans. on Very Large Scale Integration (VLSI) Systems 14(2) (2006) 193\u2013202","journal-title":"IEEE Trans. on Very Large Scale Integration (VLSI) Systems"},{"doi-asserted-by":"crossref","unstructured":"Elm, M., Kochte, M.A., Wunderlich, H.J.: On determining the real output Xs by SAT-based reasoning. In: IEEE Asian Test Symposium (ATS). (2010) 39\u201344","key":"5_CR19","DOI":"10.1109\/ATS.2010.16"},{"issue":"4","key":"5_CR20","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1109\/TCAD.2010.2042905","volume":"29","author":"H.Z. Chou","year":"2010","unstructured":"Chou, H.Z., Chang, K.H., Kuo, S.Y.: Accurately handle don\u2019t-care conditions in high-level designs and application for reducing initialized registers. IEEE Trans. on Computer-Aided Design 29(4) (2010) 646\u2013651","journal-title":"IEEE Trans. on Computer-Aided Design"},{"doi-asserted-by":"crossref","unstructured":"Wilson, C., Dill, D., Bryant, R.: Symbolic simulation with approximate values. In Hunt, W., Johnson, S., eds.: Int\u2019l Conf. on Formal Methods in Computer Aided Design (FMCAD). Vol.\u00a01954 of LNCS. Springer (2000) 507\u2013522","key":"5_CR21","DOI":"10.1007\/3-540-40922-X_29"},{"issue":"12","key":"5_CR22","doi-asserted-by":"publisher","first-page":"1908","DOI":"10.1109\/TCAD.2012.2210422","volume":"31","author":"M.A. Kochte","year":"2012","unstructured":"Kochte, M.A., Elm, M., Wunderlich, H.J.: Accurate X-propagation for test applications by SAT-based reasoning. IEEE Trans. on Computer-Aided Design 31(12) (2012) 1908\u20131919","journal-title":"IEEE Trans. on Computer-Aided Design"},{"doi-asserted-by":"crossref","unstructured":"Hillebrecht, S., Kochte, M.A., Wunderlich, H.J., Becker, B.: Exact stuck-at fault classification in presence of unknowns. In: European Test Symposium (ETS). (2012) 1\u20136","key":"5_CR23","DOI":"10.1109\/ETS.2012.6233017"},{"doi-asserted-by":"crossref","unstructured":"Erb, D., Kochte, M.A., Sauer, M., Hillebrecht, S., Schubert, T., Wunderlich, H.J., Becker, B.: Exact logic and fault simulation in presence of unknowns. ACM Trans. on Design Automation of Electronic Systems (TODAES) 19(3) (2014)","key":"5_CR24","DOI":"10.1145\/2611760"},{"unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T., eds. Frontiers in Artificial Intelligence and Applications 185. In: Handbook of Satisfiability. IOS Press (2009)","key":"5_CR25"},{"doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: IEEE\/ACM Int\u2019l Conf. on Computer Aided Design (ICCAD). (2002) 442\u2013449","key":"5_CR26","DOI":"10.1145\/774572.774637"},{"doi-asserted-by":"crossref","unstructured":"Biere, A.: Resolve and expand. In: Int\u2019l Conf. on Theory and Applications of Satisfiability Testing (SAT). Vol.\u00a03542 of LNCS, Springer (2005) 59\u201370","key":"5_CR27","DOI":"10.1007\/11527695_5"},{"doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: An effective preprocessor for QBFs based on equivalence reasoning. In: Int\u2019l Conf. on Theory and Applications of Satisfiability Testing (SAT). Vol.\u00a06175 of LNCS. Springer (2010) 85\u201398","key":"5_CR28","DOI":"10.1007\/978-3-642-14186-7_9"},{"doi-asserted-by":"crossref","unstructured":"Bloem, R., Konighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: Int\u2019l Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI). Vol.\u00a08318 of LNCS, Springer (2014) 1\u201320","key":"5_CR29","DOI":"10.1007\/978-3-642-54013-4_1"},{"doi-asserted-by":"crossref","unstructured":"Bloem, R., Egly, U., Klampfl, P., Konighofer, R., Lonsing, F.: SAT-based methods for circuit synthesis. In: Int\u2019l Conf. on Formal Methods in Computer Aided Design (FMCAD), IEEE (2014) 31\u201334","key":"5_CR30","DOI":"10.1109\/FMCAD.2014.6987592"},{"doi-asserted-by":"crossref","unstructured":"Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: ACM\/IEEE Design Automation Conference (DAC), ACM Press (2001) 238\u2013243","key":"5_CR31","DOI":"10.1145\/378239.378471"},{"doi-asserted-by":"crossref","unstructured":"Jo, S., Matsumoto, T., Fujita, M.: SAT-based automatic rectification and debugging of combinational circuits with LUT insertions. In: IEEE Asian Test Symposium (ATS), Niigata, Japan, IEEE Computer Society (2012) 19\u201324","key":"5_CR32","DOI":"10.1109\/ATS.2012.55"},{"doi-asserted-by":"crossref","unstructured":"Jo, S., Gharehbaghi, A.M., Matsumoto, T., Fujita, M.: Debugging processors with advanced features by reprogramming LUTs on FPGA. In: Int\u2019l Conf. on Field-Programmable Technology (FPT), Kyoto, Japan, IEEE (2013) 50\u201357","key":"5_CR33","DOI":"10.1109\/FPT.2013.6718329"},{"issue":"10","key":"5_CR34","doi-asserted-by":"publisher","first-page":"1606","DOI":"10.1109\/TCAD.2005.852031","volume":"24","author":"A. Smith","year":"2005","unstructured":"Smith, A., Veneris, A.G., Ali, M.F., Viglas, A.: Fault diagnosis and logic debugging using boolean satisfiability. IEEE Trans. on CAD of Integrated Circuits and Systems 24(10) (2005) 1606\u20131621","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"doi-asserted-by":"crossref","unstructured":"S\u00fclflow, A., Fey, G., Drechsler, R.: Using QBF to increase accuracy of SAT-based debugging. In: Int\u2019l Symposium on Circuits and Systems (ISCAS), Paris, France, IEEE (2010) 641\u2013644","key":"5_CR35","DOI":"10.1109\/ISCAS.2010.5537506"},{"key":"5_CR36","first-page":"396","volume-title":"IEEE Int\u2019l Conf. on Computer Design (ICCD), Asheville, NC","author":"K. Gitina","year":"2013","unstructured":"Gitina, K., Reimer, S., Sauer, M., Wimmer, R., Scholl, C., Becker, B.: Equivalence checking of partial designs using dependency quantified Boolean formulae. In: IEEE Int\u2019l Conf. on Computer Design (ICCD), Asheville, NC, USA, IEEE Computer Society (2013) 396\u2013403"},{"issue":"2","key":"5_CR37","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. on Programming Languages and Systems 8(2) (1986) 244\u2013263","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"6","key":"5_CR38","doi-asserted-by":"publisher","first-page":"1234","DOI":"10.1109\/TC.2012.53","volume":"62","author":"T. Nopper","year":"2013","unstructured":"Nopper, T., Scholl, C.: Symbolic model checking for incomplete designs with flexible modeling of unknowns. IEEE Trans. on Computers 62(6) (2013) 1234\u20131254","journal-title":"IEEE Trans. on Computers"},{"doi-asserted-by":"crossref","unstructured":"Miller, C., Kupferschmid, S., Lewis, M.D.T., Becker, B.: Encoding techniques, craig interpolants and bounded model checking for incomplete designs. In: Int\u2019l Conf. on Theory and Applications of Satisfiability Testing (SAT). Vol.\u00a06175 of LNCS, Springer (2010) 194\u2013208","key":"5_CR39","DOI":"10.1007\/978-3-642-14186-7_17"},{"doi-asserted-by":"crossref","unstructured":"Miller, C., Scholl, C., Becker, B.: Proving QBF-hardness in bounded model checking for incomplete designs. In: Int\u2019l Workshop on Microprocessor Test and Verification (MTV), IEEE Computer Society (2013)","key":"5_CR40","DOI":"10.1109\/MTV.2013.11"},{"doi-asserted-by":"crossref","unstructured":"Sauer, M., Reimer, S., Polian, I., Schubert, T., Becker, B.: Provably Optimal Test Cube Generation Using Quantified Boolean Formula Solving. In: Asia and South Pacific Design Automation Conference (ASPDAC). (2013) 533\u2013539","key":"5_CR41","DOI":"10.1109\/ASPDAC.2013.6509651"},{"doi-asserted-by":"crossref","unstructured":"Reimer, S., Sauer, M., Schubert, T., Becker, B.: Using maxbmc for pareto-optimal circuit initialization. In: Int\u2019l Conf. on Design, Automation & Test in Europe (DATE), IEEE (2014) 1\u20136","key":"5_CR42","DOI":"10.7873\/DATE2014.161"},{"doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Annual ACM Symposium on Theory of Computing (STOC), ACM (1971) 151\u2013158","key":"5_CR43","DOI":"10.1145\/800157.805047"},{"doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time (preliminary report). In: Annual ACM Symposium on Theory of Computing (STOC), New York, NY , USA, ACM (1973) 1\u20139","key":"5_CR44","DOI":"10.1145\/800125.804029"},{"doi-asserted-by":"crossref","unstructured":"Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.: Solving DQBF through quantifier elimination. In: Int\u2019l Conf. on Design, Automation & Test in Europe (DATE), Grenoble, France, IEEE (2015)","key":"5_CR45","DOI":"10.7873\/DATE.2015.0098"},{"unstructured":"Fr\u00f6hlich, A., Kovasznai, G., Biere, A., Veith, H.: iDQ: Instantiation-based DQBF solving. In: Intl. Workshop on Pragmatics of SAT (POS), Vienna, Austria (2014)","key":"5_CR46"},{"doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic Part 2 (1970) 115\u2013125","key":"5_CR47","DOI":"10.1007\/978-1-4899-5327-8_25"},{"unstructured":"Turpin, M.: The dangers of living with an X (bugs hidden in your Verilog). In: Boston Synopsys Users Group Meeting. (2003) 1\u201334","key":"5_CR48"},{"doi-asserted-by":"crossref","unstructured":"Ulrich, E.G., Baker, T.: The concurrent simulation of nearly identical digital networks. In: Papers on Twenty-five years of electronic design automation. 25 years of DAC (1988) 318\u2013323","key":"5_CR49","DOI":"10.1145\/62882.62918"},{"issue":"12","key":"5_CR50","first-page":"20","volume":"6","author":"J. Waicukauski","year":"1985","unstructured":"Waicukauski, J., Eichelberger, E., Forlenza, D., Lindbloom, E., McCarthy, T.: Fault simulation for structured VLSI. VLSI Systems Design 6(12) (1985) 20\u201332","journal-title":"VLSI Systems Design"},{"issue":"5","key":"5_CR51","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1109\/TCAD.1987.1270316","volume":"6","author":"K. Antreich","year":"1987","unstructured":"Antreich, K., Schulz, M.: Accelerated fault simulation and fault grading in combinational circuits. IEEE Trans. on Computer-Aided Design 6(5) (1987) 704\u2013712","journal-title":"IEEE Trans. on Computer-Aided Design"},{"unstructured":"Lee, H., Ha, D.: An efficient, forward fault simulation algorithm based on the parallel pattern single fault propagation. In: Int\u2019l Test Conference (ITC). (1991) 946\u2013955","key":"5_CR52"},{"unstructured":"Rudnick, E., Patel, J., Pomeranz, I.: On potential fault detection in sequential circuits. In: Int\u2019l Test Conference (ITC). (1996) 142\u2013149","key":"5_CR53"},{"unstructured":"Schubert, T., Lewis, M., Becker, B.: Antom\u2014solver description. SAT Race (2010)","key":"5_CR54"},{"doi-asserted-by":"crossref","unstructured":"Hillebrecht, S., Kochte, M.A., Erb, D., Wunderlich, H.J., Becker, B.: Accurate QBF-based test pattern generation in presence of unknown values. In: Int\u2019l Conf. on Design, Automation & Test in Europe (DATE). (2013) 436\u2013441","key":"5_CR55","DOI":"10.7873\/DATE.2013.098"},{"unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Annual Symposium on Foundations of Computer Science, IEEE Computer Society (1990) 746\u2013757","key":"5_CR56"},{"unstructured":"Miller, C., Nopper, T., Scholl, C.: Symbolic CTL model checking for incomplete designs by selecting property-specific subsets of local component assumptions. In: Workshop \u201cMethoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen\u201d (MBMV), Universit\u00e4tsbibliothek Berlin, Germany (2009) 87\u201396","key":"5_CR57"},{"doi-asserted-by":"crossref","unstructured":"Nopper, T., Scholl, C.: Approximate symbolic model checking for incomplete designs. In: Int\u2019l Conf. on Formal Methods in Computer Aided Design (FMCAD). Vol.\u00a03312 of LNCS, Springer (2004) 290\u2013305","key":"5_CR58","DOI":"10.1007\/978-3-540-30494-4_21"}],"container-title":["Formal Modeling and Verification of Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-658-09994-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T00:58:55Z","timestamp":1676941135000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-658-09994-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783658099930","9783658099947"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-658-09994-7_5","relation":{},"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"6 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}