{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T21:31:38Z","timestamp":1777498298071,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642029585","type":"print"},{"value":"9783642029592","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_12","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T01:02:22Z","timestamp":1248483742000},"page":"151-156","source":"Crossref","is-referenced-by-count":104,"title":["veriT: An Open, Trustable and Efficient SMT-Solver"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Bouton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Diego","family":"Caminha B. de Oliveira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"D\u00e9harbe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log.\u00a010(1) (2009)","DOI":"10.1145\/1459010.1459014"},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation\u00a0183(2), 140\u2013164 (2003)","journal-title":"Information and Computation"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability Modulo Theories Competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 20\u201323. Springer, Heidelberg (2005)"},{"issue":"2-3","key":"12_CR4","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s00165-003-0006-5","volume":"15","author":"A.L.C. Cavalcanti","year":"2003","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A Refinement Strategy for Circus. Formal Aspects of Computing\u00a015(2-3), 146\u2013181 (2003)","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"12_CR5","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2008.04.079","volume":"198","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based theory combination. Electronic Notes in Theoretical Computer Science\u00a0198(2), 37\u201349 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"12_CR6","unstructured":"de Moura, L.M., Bj\u00f6rner, N.: Proofs and refutations, and Z3. In: LPAR Workshops. CEUR Workshop Proceedings, vol.\u00a0418 (2008)"},{"key":"12_CR7","unstructured":"D\u00e9harbe, D., de Oliveira, D., Fontaine, P.: Combining decision procedures by (model-)equality propagation. In: Brazil. Symp. Formal Methods, pp. 51\u201366 (2008)"},{"key":"12_CR8","unstructured":"D\u00e9harbe, D., Ranise, S.: Bdd-driven first-order satisfiability procedures (extended version). Research report 4630, LORIA (2002)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"12_CR10","unstructured":"Fontaine, P.: Combinations of theories and the Bernays-Sch\u00f6nfinkel-Ramsey class. In: 4th Int\u2019l Verification Workshop (VERIFY) (2007)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.entcs.2005.12.003","volume":"144","author":"J. Grundy","year":"2005","unstructured":"Grundy, J., Melham, T., Krsti\u0107, S., McLaughlin, S.: Tool building requirements for an API to first-order solvers. Electronic Notes in Theoretical Computer Science\u00a0144, 15\u201326 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"key":"12_CR14","first-page":"281","volume-title":"IEEE Intl. Conf. Software Engineering and Formal Methods","author":"M. Oliveira","year":"2008","unstructured":"Oliveira, M., Gurgel, C., de Castro, A.: Crefine: Support for the Circus refinement calculus. In: IEEE Intl. Conf. Software Engineering and Formal Methods, pp. 281\u2013290. IEEE Comp. Soc. Press, Los Alamitos (2008)"},{"key":"12_CR15","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.2 (August 2006)"},{"key":"12_CR16","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-25984-8_15","volume-title":"Automated Reasoning","author":"S. Schulz","year":"2004","unstructured":"Schulz, S.: System Description: E\u00a00.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 223\u2013228. Springer, Heidelberg (2004)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Stump, A.: Proof Checking Technology for Satisfiability Modulo Theories. In: Logical Frameworks and Meta-Languages: Theory and Practice (2008)","DOI":"10.1016\/j.entcs.2008.12.121"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: System description: Spass version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T13:52:06Z","timestamp":1558446726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}