{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:53Z","timestamp":1762458593661},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540755951"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75596-8_7","type":"book-chapter","created":{"date-parts":[[2007,11,3]],"date-time":"2007-11-03T10:03:37Z","timestamp":1194084217000},"page":"66-81","source":"Crossref","is-referenced-by-count":5,"title":["Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver"],"prefix":"10.1007","author":[{"given":"David","family":"Walter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott","family":"Little","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chris","family":"Myers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"11","key":"7_CR1","doi-asserted-by":"crossref","first-page":"1356","DOI":"10.1109\/43.97615","volume":"10","author":"R.P. Kurshan","year":"1991","unstructured":"Kurshan, R.P., McMillan, K.L.: Analysis of digital circuits through symbolic reduction. IEEE Transactions on CAD\u00a010(11), 1356\u20131371 (1991)","journal-title":"IEEE Transactions on CAD"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Hartong, W., Hedrich, L., Barke, E.: Model checking algorithms for analog verification. In: Proc. of DAC, pp. 542\u2013547 (2002)","DOI":"10.1145\/514053.514055"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog designs. In: Proc. of ICCAD, pp. 210\u2013217 (2004)","DOI":"10.1109\/ICCAD.2004.1382573"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-540-30494-4_3","volume-title":"FMCAD 2004","author":"T. Dang","year":"2004","unstructured":"Dang, T., Donze, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid systems techniques. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 21\u201336. Springer, Heidelberg (2004)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Frehse, G., Krogh, B.H., Rutenbar, R.A.: Verifying analog oscillator circuits using forward\/backward refinement. In: Proc. of DATE, pp. 257\u2013262 (2006)","DOI":"10.1109\/DATE.2006.244113"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Little, S., Seegmiller, N., Walter, D., Myers, C.J.: Verification of analog\/mixed-signal circuits using labeled hybrid petri nets. In: Proc. of ICCAD, pp. 275\u2013282 (2006)","DOI":"10.1109\/ICCAD.2006.320148"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Walter, D., Little, S., Seegmiller, N., Myers, C., Yoneda, T.: Symbolic model checking of analog\/mixed-signal circuits. In: Proc. of ASPDAC, pp. 316\u2013323 (2007)","DOI":"10.1109\/ASPDAC.2007.358005"},{"issue":"6","key":"7_CR8","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/10720246_8","volume-title":"Recent Advances in AI Planning","author":"A. Armando","year":"2000","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol.\u00a01809, pp. 97\u2013108. Springer, Heidelberg (2000)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"SAT 2004","author":"A. Armando","year":"2005","unstructured":"Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: A sat-based decision procedure for the boolean combination of difference constraints. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, Springer, Heidelberg (2005)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 2002","author":"C. Barrett","year":"2002","unstructured":"Barrett, C., Dill, D., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to sat. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/978-3-540-31980-1_21","volume-title":"TACAS 2005.","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 317\u2013333. Springer, Heidelberg (2005)"},{"key":"7_CR13","unstructured":"de Moura, L., Rue, H.: Lemmas on demand for satisfiability solvers. In: Proc. of SAT (2002)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.C., Owre, S., Rue, H.: ICS: Integrated Canonization and Solving (Tool presentation). In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"CAV","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/11691617_9","volume-title":"SPIN 2006","author":"A. Armando","year":"2006","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using smt solvers instead of sat solvers. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 146\u2013162. Springer, Heidelberg (2006)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/11513988_34","volume-title":"CAV.","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient satisfiability modulo theories via delayed theory combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 335\u2013349. Springer, Heidelberg (2005)"},{"key":"7_CR18","series-title":"Lecture Notes in Artificial Intelligence","first-page":"36","volume-title":"LPAR 2004","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and Abstract DPLL Modulo Theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 36\u201350. Springer, Heidelberg (2005)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"CAV 2006","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"3","key":"7_CR20","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.entcs.2006.02.018","volume":"153","author":"C.J. Myers","year":"2006","unstructured":"Myers, C.J., Harrison, R.R., Walter, D., Seegmiller, N., Little, S.: The case for analog circuit verification. Electronic Notes Theoretical Computer Science\u00a0153(3), 53\u201363 (2006)","journal-title":"Electronic Notes Theoretical Computer Science."},{"key":"7_CR21","unstructured":"Zheng, H.: Specification and compilation of timed systems. Master\u2019s thesis, University of Utah (1998)"},{"key":"7_CR22","doi-asserted-by":"crossref","DOI":"10.1002\/0471224146","volume-title":"Asynchronous Circuit Design","author":"C. Myers","year":"2001","unstructured":"Myers, C.: Asynchronous Circuit Design. Wiley, Chichester (2001)"},{"key":"7_CR23","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1023\/A:1008330914786","volume":"11","author":"R. David","year":"2001","unstructured":"David, R., Alla, H.: On hybrid petri nets. Discrete Event Dynamic Systems: Theory and Applications\u00a011, 9\u201340 (2001)","journal-title":"Discrete Event Dynamic Systems: Theory and Applications"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Hybrid Systems, pp. 209\u2013229 (1992)","DOI":"10.1007\/3-540-57318-6_30"},{"key":"7_CR25","unstructured":"Walter, D.: Verification of Analog and Mixed-Signal Circuits Using Symbolic Methods. PhD thesis, University of Utah (2007)"},{"key":"7_CR26","first-page":"394","volume-title":"7th Symposium of Logics in Computer Science","author":"T. Henzinger","year":"1992","unstructured":"Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: 7th Symposium of Logics in Computer Science, pp. 394\u2013406. IEEE Computer Scienty Press, Los Alamitos (1992)"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1007\/3-540-58152-9_23","volume-title":"PNPM 1994","author":"E. Pastor","year":"1994","unstructured":"Pastor, E., Roig, O., Cortadella, J., Badia, R.M.: Petri net analysis using boolean manipulation. In: Valette, R. (ed.) PNPM 1994. LNCS, vol.\u00a0815, pp. 416\u2013435. Springer, Heidelberg (1994), citeseer.ist.psu.edu\/pastor94petri.html"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"TACAS 2003","author":"K. McMillan","year":"2003","unstructured":"McMillan, K., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75596-8_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:25:31Z","timestamp":1619504731000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75596-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755951"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75596-8_7","relation":{},"subject":[]}}