{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T21:50:55Z","timestamp":1743112255155,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175232"},{"type":"electronic","value":"9783319175249"}],"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-319-17524-9_22","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"310-326","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Integrating SMT with Theorem Proving for Analog\/Mixed-Signal Circuit Verification"],"prefix":"10.1007","author":[{"given":"Yan","family":"Peng","sequence":"first","affiliation":[]},{"given":"Mark","family":"Greenstreet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). http:\/\/dx.doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Moore, J., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Kundert, K.S.: Introduction to RF simulation and its application. IEEE J. Solid-State Circuits 34(9), 1298\u20131319 (1999). http:\/\/dx.doi.org\/10.1109\/4.782091","DOI":"10.1109\/4.782091"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Kim, J., Jeeradit, M., Lim, B., Horowitz, M.A.: Leveraging designer\u2019s intent: a path toward simpler analog CAD tools. In: Custom Integrated Circuits Conf., pp. 613\u2013620, September 2009. http:\/\/dx.doi.org\/10.1109\/CICC.2009.5280741","DOI":"10.1109\/CICC.2009.5280741"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. In: 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning, pp. 43\u201351. http:\/\/dx.doi.org\/10.1016\/j.entcs.2005.12.005","DOI":"10.1016\/j.entcs.2005.12.005"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167\u2013181. Springer, Heidelberg (2006). http:\/\/dx.doi.org\/10.1007\/11691372_11","DOI":"10.1007\/11691372_11"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48\u201362. Springer, Heidelberg (2007). http:\/\/dx.doi.org\/10.1007\/978-3-540-74464-1_4","DOI":"10.1007\/978-3-540-74464-1_4"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135\u2013150. Springer, Heidelberg (2011). http:\/\/dx.doi.org\/10.1007\/978-3-642-25379-9_12","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-28717-6_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Merz","year":"2012","unstructured":"Merz, S., Vanzetto, H.: Automatic verification of TLA$${^ + }$$ proof obligations with SMT solvers. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 289\u2013303. Springer, Heidelberg (2012). https:\/\/hal.inria.fr\/hal-00760570\/document"},{"issue":"1","key":"22_CR10","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. of Automated Reasoning 51(1), 109\u2013128 (2013). http:\/\/dx.doi.org\/10.1007\/s10817-013-9278-5","journal-title":"J. of Automated Reasoning"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyof, Y., Voisin, L.: Integrating SMT solvers in Rodin. Science of Computer Programming 94(pt. 2), 130\u2013143 (2014). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S016764231400183X","DOI":"10.1016\/j.scico.2014.04.012"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"CW Barrett","year":"2004","unstructured":"Barrett, C.W., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588\u2013605. Springer, Heidelberg (2006). http:\/\/dx.doi.org\/10.1007\/11901433_32","DOI":"10.1007\/11901433_32"},{"key":"22_CR14","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard version 2.0. In: 8th SMT Workshop (2010). http:\/\/smtlib.cs.uiowa.edu\/papers\/smt-lib-reference-v2.0-r10.12.21.pdf"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-319-06200-6_9","volume-title":"NASA Formal Methods","author":"F Immler","year":"2014","unstructured":"Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 113\u2013127. Springer, Heidelberg (2014). http:\/\/home.in.tum.de\/\u00a0immler\/documents\/immler2014enclosures.pdf"},{"key":"22_CR16","unstructured":"Harutunian, S.: Formal verification of computer controlled systems. Ph.D. dissertation, University of Texas, Austin, May 2007. http:\/\/www.lib.utexas.edu\/etd\/d\/2007\/harutunians68792\/harutunians68792.pdf"},{"issue":"11","key":"22_CR17","doi-asserted-by":"publisher","first-page":"1356","DOI":"10.1109\/43.97615","volume":"10","author":"R Kurshan","year":"1991","unstructured":"Kurshan, R., McMillan, K.: Analysis of digital circuits through symbolic reduction. IEEE Trans. CAD 10(11), 1356\u20131371 (1991). http:\/\/dx.doi.org\/10.1109\/43.97615","journal-title":"IEEE Trans. CAD"},{"key":"22_CR18","unstructured":"Hedrich, L., Barke, E.: A formal approach to nonlinear analog circuit verification. In: ICCAD, pp. 123\u2013127 (1995). http:\/\/dl.acm.org\/citation.cfm?id=224841.224870"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Greenstreet, M. R.: Verifying safety properties of differential equations. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 277\u2013287. Springer, Heidelberg (1996). http:\/\/dx.doi.org\/10.1007\/3-540-61474-5_76","DOI":"10.1007\/3-540-61474-5_76"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Hartong, W., Hedrich, L., Barke, E.: Model checking algorithms for analog verification. In: 39th DAC, pp. 542\u2013547, June 2002. http:\/\/dx.doi.org\/10.1109\/DAC.2002.1012684","DOI":"10.1145\/513918.514055"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Dang, T., Donz\u00e9, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid system techniques. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 21\u201336. Springer, Heidelberg (2004). http:\/\/dx.doi.org\/10.1007\/978-3-540-30494-4_3","DOI":"10.1007\/978-3-540-30494-4_3"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Dong, Z.J., Zaki, M.H., Al-Sammane, G., Tahar, S., Bois, G.: Checking properties of PLL designs using run-time verification. In: Int\u2019l. Conf. Microelectronics, pp. 125\u2013128 (2007). http:\/\/dx.doi.org\/10.1109\/ICM.2007.4497676","DOI":"10.1109\/ICM.2007.4497676"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Jesser, A., Hedrich, L.: A symbolic approach for mixed-signal model checking. In: ASPDAC, pp. 404\u2013409 (2008). http:\/\/dl.acm.org\/citation.cfm?id=1356802.1356903","DOI":"10.1109\/ASPDAC.2008.4483984"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Althoff, M., Rajhans, A., et al.: Formal verification of phase-locked loops using reachability analysis and continuization. Comm. ACM 56(10), 97\u2013104 (2013). http:\/\/doi.acm.org\/10.1145\/2507771.2507783","DOI":"10.1145\/2507771.2507783"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Lin, H., Li, P., Myers, C. J.: Verification of digitally-intensive analog circuits via kernel ridge regression and hybrid reachability analysis. In: 50th DAC, pp. 66:1\u201366:6 (2013). http:\/\/doi.acm.org\/10.1145\/2463209.2488814","DOI":"10.1145\/2463209.2488814"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Lin, H., Li, P.: Parallel hierarchical reachability analysis for analog verification. In: 51st DAC, pp. 150:1\u2013150:6 (2014). http:\/\/doi.acm.org\/10.1145\/2593069.2593178","DOI":"10.1145\/2593069.2593178"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). http:\/\/dx.doi.org\/10.1007\/978-3-642-22110-1_30","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"Wei, J., Peng, Y., Yu, G., Greenstreet, M.: Verifying global convergence for a digital phase-locked loop. In: 13th FMCAD, pp. 113\u2013120, October 2013. http:\/\/dx.doi.org\/10.1109\/FMCAD.2013.6679399","DOI":"10.1109\/FMCAD.2013.6679399"},{"issue":"5","key":"22_CR29","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J Marques-Silva","year":"1999","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Computers 48(5), 506\u2013521 (1999). http:\/\/dx.doi.org\/10.1109\/12.769433","journal-title":"IEEE Trans. Computers"},{"key":"22_CR30","unstructured":"Gamboa, R.: Mechanically verified real-valued algorithms in ACL2. Ph.D. dissertation, University of Texas at Austin (1999)"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Crossley, J., Naviasky, E., Alon, E.: An energy-efficient ring-oscillator digital PLL. In: Custom Integrated Circuits Conf. (September 2010). http:\/\/dx.doi.org\/10.1109\/CICC.2010.5617417","DOI":"10.1109\/CICC.2010.5617417"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T00:46:22Z","timestamp":1676940382000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}