{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:57:53Z","timestamp":1759147073739,"version":"3.28.0"},"reference-count":25,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,3]]},"DOI":"10.1109\/date.2011.5763035","type":"proceedings-article","created":{"date-parts":[[2013,2,19]],"date-time":"2013-02-19T22:45:16Z","timestamp":1361313916000},"page":"1-6","source":"Crossref","is-referenced-by-count":28,"title":["STABLE: A new QF-BV SMT solver for hard verification problems combining Boolean reasoning with computer algebra"],"prefix":"10.1109","author":[{"given":"Evgeny","family":"Pavlenko","sequence":"first","affiliation":[{"name":"Dept. of Electrical and Computer Eng., University of Kaiserslautern, Germany"}]},{"given":"Markus","family":"Wedler","sequence":"additional","affiliation":[{"name":"Dept. of Electrical and Computer Eng., University of Kaiserslautern, Germany"}]},{"given":"Dominik","family":"Stoffel","sequence":"additional","affiliation":[{"name":"Dept. of Electrical and Computer Eng., University of Kaiserslautern, Germany"}]},{"given":"Wolfgang","family":"Kunz","sequence":"additional","affiliation":[{"name":"Dept. of Electrical and Computer Eng., University of Kaiserslautern, Germany"}]},{"given":"Alexander","family":"Dreyer","sequence":"additional","affiliation":[{"name":"Dept. of System Analysis, Prognosis and Control, Fraunhofer ITWM, Kaiserslautern, Germany"}]},{"given":"Frank","family":"Seelisch","sequence":"additional","affiliation":[{"name":"Dept. of Mathematics, University of Kaiserslautern, Germany"}]},{"given":"Gert-Martin","family":"Greuel","sequence":"additional","affiliation":[{"name":"Dept. of Mathematics, University of Kaiserslautern, Germany"}]}],"member":"263","reference":[{"key":"ref10","article-title":"The SMT-LIB Standard: Version 2.0","author":"barrett","year":"2010","journal-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh England)"},{"key":"ref11","first-page":"81","article-title":"A Fast Linear-Arithmetic Solver for DPLL(T)","volume":"4144","author":"dutertre","year":"2006","journal-title":"Proc International Conference Computer Aided Verification (CAV) Ser LNCS"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","article-title":"Efficient e-matching for SMT solvers","volume":"4603","author":"de moura","year":"2007","journal-title":"CADE Ser Lecture Notes in Computer Science"},{"key":"ref13","article-title":"Spear Theorem Prover","author":"babi\u00f3","year":"2008","journal-title":"SAT-Race 2008"},{"key":"ref14","article-title":"Boolector: An efficient SMT solver for bit-vectors and arrays","author":"brummayer","year":"2009","journal-title":"Proc Intl Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_54"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"year":"0","key":"ref17","article-title":"STP"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.888277"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/FDL.2008.4641433"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_18"},{"journal-title":"OneSpin 360MV","article-title":"Onespin Solutions GmbH, Germany","year":"0","key":"ref3"},{"key":"ref6","article-title":"An extensible SAT-solver","author":"een","year":"2003","journal-title":"Proc Theory Applications Satisfiability Testing (SAT)"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2002.998262"},{"key":"ref8","first-page":"825","volume":"185","author":"barrett","year":"2009","journal-title":"Satisfiability Modulo Theories Ser Frontiers in Artificial Intelligence and Applications"},{"journal-title":"PrecoSAT 236","year":"0","key":"ref7"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2007.907270"},{"journal-title":"The Satisfiability Modulo Theories Library (SMT-LIB)","year":"2006","author":"ranise","key":"ref9"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"ref20","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/978-3-540-70545-1_45","article-title":"An algebraic approach for proving data correctness in arithmetic data paths","author":"wienand","year":"2008","journal-title":"Proc International Conference Computer Aided Verification (CAV)"},{"key":"ref22","first-page":"705","author":"greuel","year":"2007","journal-title":"A Singular Introduction to Commutative Algebra"},{"journal-title":"An Introduction to Gröbner Bases","year":"2003","author":"adams","key":"ref21"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2008.11.043"},{"journal-title":"Standard bases over rings and applications","year":"2010","author":"wienand","key":"ref23"},{"year":"2009","key":"ref25","article-title":"SMT-COMP"}],"event":{"name":"2011 Design, Automation & Test in Europe Conference & Exhibition (DATE 2011)","start":{"date-parts":[[2011,3,14]]},"location":"Grenoble, France","end":{"date-parts":[[2011,3,18]]}},"container-title":["2011 Design, Automation & Test in Europe"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5754459\/5762992\/05763035.pdf?arnumber=5763035","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T14:21:49Z","timestamp":1623162109000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/5763035\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3]]},"references-count":25,"URL":"https:\/\/doi.org\/10.1109\/date.2011.5763035","relation":{},"subject":[],"published":{"date-parts":[[2011,3]]}}}