{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T04:11:17Z","timestamp":1706760677240},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2016,6,17]],"date-time":"2016-06-17T00:00:00Z","timestamp":1466121600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s10009-016-0426-1","type":"journal-article","created":{"date-parts":[[2016,6,17]],"date-time":"2016-06-17T06:26:41Z","timestamp":1466144801000},"page":"605-621","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["metaSMT: focus on your application and not on solver integration"],"prefix":"10.1007","volume":"19","author":[{"given":"Heinz","family":"Riener","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Finn","family":"Haedicke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Frehse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias","family":"Soeken","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Gro\u00dfe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Goerschwin","family":"Fey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,17]]},"reference":[{"key":"426_CR1","unstructured":"Aiger http:\/\/fmv.jku.at\/aiger\/"},{"key":"426_CR2","doi-asserted-by":"crossref","unstructured":"Abdessaied, N., Soeken, M., Wille, R., Drechsler, R.: Exact template matching using boolean satisfiability. In: IEEE International Symposium on Multiple-Valued Logic, pp. 328\u2013333 (2013)","DOI":"10.1109\/ISMVL.2013.26"},{"key":"426_CR3","doi-asserted-by":"crossref","unstructured":"Arbel, E., Rokhlenko, O., Yorav, K.: SAT-based synthesis of clock gating functions using 3-valued abstraction. In: Formal Methods in, Computer-Aided Design, pp. 198\u2013204 (2009)","DOI":"10.1109\/FMCAD.2009.5351118"},{"issue":"1","key":"426_CR4","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transf. 11(1), 69\u201383 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"426_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Computer Aided Verification, pp. 171\u2013177 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"426_CR6","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0 (2012)"},{"key":"426_CR7","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli C.: Handbook of Satisfiability, chapter Satisfiability Modulo Theories, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"issue":"2\u20134","key":"426_CR8","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. J. Satisfiab. Boolean Model Comput. 4(2\u20134), 75\u201397 (2008)","journal-title":"J. Satisfiab. Boolean Model Comput."},{"key":"426_CR9","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. In: Theory and Applications of Satisfiability Testing, pp. 51\u201352 (2013)"},{"key":"426_CR10","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 193\u2013207 (1999)","DOI":"10.21236\/ADA360973"},{"key":"426_CR11","doi-asserted-by":"crossref","unstructured":"Bjesse, P.: A practical approach to word level model checking of industrial netlists. In: Computer Aided Verification, pp. 446\u2013458 (2008)","DOI":"10.1007\/978-3-540-70545-1_43"},{"key":"426_CR12","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Boolector, A.Biere: An efficient SMT solver for bit-vectors and arrays. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 174\u2013177 (2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"426_CR13","unstructured":"Bruttomesso, R., Cok, D.R., Griggio, A.: Satisfiability modulo theories competition (SMT-LIB) 2013: rules and procedures, 2012. This version revised, pp. 6\u20132 (2012)"},{"key":"426_CR14","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: jSMTLIB: tutorial, validation and adapter tools for SMT-LIBv2. In: NASA Formal Methods, pp. 480\u2013486 (2011)","DOI":"10.1007\/978-3-642-20398-5_36"},{"key":"426_CR15","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Symposium on the Theory of, Computing, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"426_CR16","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"7","key":"426_CR17","doi-asserted-by":"crossref","first-page":"1329","DOI":"10.1109\/TCAD.2008.923107","volume":"27","author":"R Drechsler","year":"2008","unstructured":"Drechsler, R., Eggersgl\u00fc\u00df, S., Fey, G., Glowatz, A., Hapke, F., Schl\u00f6ffel, J., Tille, D.: On acceleration of SAT-based ATPG for industrial designs. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 27(7), 1329\u20131333 (2008)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circ. Syst."},{"key":"426_CR18","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Theory and Applications of Satisfiability Testing, pp. 502\u2013518 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"426_CR19","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: International Conference on Computer Aided Design, pp. 794\u2013801 (2006)","DOI":"10.1109\/ICCAD.2006.320122"},{"key":"426_CR20","doi-asserted-by":"crossref","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Computer Aided Verification, pp. 519\u2013531 (2007)","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"426_CR21","doi-asserted-by":"crossref","unstructured":"Haedicke, F., Alizadeh, B., Fey, G., Fujita, M., Drechsler, R.: Polynomial datapath optimization using constraint solving and formal modelling. In: International Conference on Computer Aided Design, pp. 756\u2013761 (2010)","DOI":"10.1109\/ICCAD.2010.5654279"},{"key":"426_CR22","doi-asserted-by":"crossref","unstructured":"Haedicke, F., Le, H.M., Groe, D., Drechsler, R.: CRAVE: an advanced constrained random verification environment for SystemC. In: International Symposium on System-on-Chip, pp. 1\u20137 (2012)","DOI":"10.1109\/ISSoC.2012.6376356"},{"key":"426_CR23","doi-asserted-by":"crossref","unstructured":"Hudak, P.R.: Modular domain specific languages and tools. In: International Conference on Software Reuse, pp. 134 (1998)","DOI":"10.1109\/ICSR.1998.685738"},{"key":"426_CR24","unstructured":"Levin, L.A.: Universal search problems. Problems of Information Transmission. Translation from Russian to English, 9(3), 115\u2013116 (1973)"},{"key":"426_CR25","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Computer Aided Verification, pp. 1\u201313 (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"issue":"1\u20134","key":"426_CR26","first-page":"1","volume":"2","author":"NS Niklas E\u00e9n","year":"2006","unstructured":"Niklas E\u00e9n, N.S.: Translating pseudo-boolean constraints into SAT. J. Satisfiab. Boolean Model. Comput. 2(1\u20134), 1\u201326 (2006)","journal-title":"J. Satisfiab. Boolean Model. Comput."},{"key":"426_CR27","doi-asserted-by":"crossref","unstructured":"Palikareva, H., Cadar, C.: Multi-solver support in symbolic execution. In: Computer Aided Verification, pp. 53\u201368 (2013)","DOI":"10.1007\/978-3-642-39799-8_3"},{"issue":"1","key":"426_CR28","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"key":"426_CR29","doi-asserted-by":"crossref","unstructured":"Riener, H., Bloem, R., Fey, G.: Test case generation from mutants using model checking techniques. In: International Conference on Software Testing, Verification, and Validation Workshops, pp. 388\u2013397 (2011)","DOI":"10.1109\/ICSTW.2011.55"},{"key":"426_CR30","doi-asserted-by":"crossref","unstructured":"Riener, H., Fey, G.: Model-based diagnosis versus error explanation. In: International Conference on Formal Methods and Models for Co-Design, pp. 43\u201352 (2012)","DOI":"10.1109\/MEMCOD.2012.6292299"},{"key":"426_CR31","doi-asserted-by":"crossref","unstructured":"Riener, H., Frehse, S., Fey, G.: Improving fault tolerance utilizing hardware-software-co-synthesis. In: Design, Automation, and Test in Europe, pp. 939\u2013942 (2013)","DOI":"10.7873\/DATE.2013.197"},{"key":"426_CR32","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.4.1. University of Colorado at Boulder, Boulder (2009)"},{"key":"426_CR33","doi-asserted-by":"crossref","unstructured":"Strichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Correct Hardware Design and Verification Methods, pp. 58\u201370 (2001)","DOI":"10.1007\/3-540-44798-9_4"},{"key":"426_CR34","doi-asserted-by":"crossref","unstructured":"Wille, R., Fey, G., Gro\u00dfe, D., Eggersgl\u00fc\u00df S., Drechsler, R.: Sword: A SAT like prover using word level information. In: IFIP\/IEEE International Conference on Very Large Scale Integration, pp. 88\u201393 (2007)","DOI":"10.1109\/VLSISOC.2007.4402478"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-016-0426-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0426-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0426-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0426-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T12:01:51Z","timestamp":1600776111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-016-0426-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,17]]},"references-count":34,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["426"],"URL":"https:\/\/doi.org\/10.1007\/s10009-016-0426-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6,17]]}}}