{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:05:15Z","timestamp":1742915115121,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642043673"},{"type":"electronic","value":"9783642043680"}],"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-04368-0_1","type":"book-chapter","created":{"date-parts":[[2009,9,2]],"date-time":"2009-09-02T07:31:59Z","timestamp":1251876719000},"page":"1-6","source":"Crossref","is-referenced-by-count":0,"title":["Tapas: Theory Combinations and Practical Applications"],"prefix":"10.1007","author":[{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"first","affiliation":[]},{"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Spanish tapas, http:\/\/en.wikipedia.org\/wiki\/Tapas"},{"key":"1_CR2","unstructured":"Bj\u00f8rner, N., Dutertre, B., de Moura, L.: Accelerating DPLL(T) using Joins - DPLL(\u2294). In: LPAR 2008 (2008)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","volume-title":"TACAS 2009","author":"N. Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 307\u2013321. Springer, Heidelberg (2009)"},{"key":"1_CR4","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1145\/1180405.1180445","volume-title":"CCS","author":"C. Cadar","year":"2006","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: Exe: automatically generating inputs of death. In: CCS, pp. 322\u2013335. ACM Press, New York (2006)"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/1346281.1346322","volume-title":"ASPLOS XIII: Proceedings of the 13th international conference on Architectural support for programming languages and operating systems","author":"M. Castro","year":"2008","unstructured":"Castro, M., Costa, M., Martin, J.-P.: Better bug reporting with better privacy. In: ASPLOS XIII: Proceedings of the 13th international conference on Architectural support for programming languages and operating systems, pp. 319\u2013328. ACM, New York (2008)"},{"key":"1_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L. Moura de","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"1_CR7","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based Theory Combination. In: SMT 2007 (2007)"},{"key":"1_CR8","unstructured":"de Moura, L., Bj\u00f8rner, N.: Relevancy Propagation. Technical Report MSR-TR-2007-140, Microsoft Research (2007)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"1_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-540-71070-7_35","volume-title":"Automated Reasoning","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 410\u2013425. Springer, Heidelberg (2008)"},{"key":"1_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-71070-7_40","volume-title":"Automated Reasoning","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 475\u2013490. Springer, Heidelberg (2008)"},{"issue":"5","key":"1_CR12","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1109\/MS.2008.109","volume":"25","author":"P. Godefroid","year":"2008","unstructured":"Godefroid, P., de Halleux, J., Nori, A.V., Rajamani, S.K., Schulte, W., Tillmann, N., Levin, M.Y.: Automating Software Testing Using Program Analysis. IEEE Software\u00a025(5), 30\u201337 (2008)","journal-title":"IEEE Software"},{"issue":"7","key":"1_CR13","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Lynch, C., de Moura, L.: On deciding satisfiability by DPLL(\u0393\u2009+\u2009T) and unsound theorem proving. In: CADE (2009)","DOI":"10.1007\/978-3-642-02959-2_3"},{"key":"1_CR15","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, pp. 21\u201328 (1962)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Hendrix, J.: Linear Functional Fixed-points. In: CAV (2009)","DOI":"10.1007\/978-3-642-02658-4_13"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/11817963_38","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2006","unstructured":"Sen, K., Agha, G.A.: CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 419\u2013423. Springer, Heidelberg (2006)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified SMT formulas. In: CAV (2009)","DOI":"10.1007\/978-3-642-02658-4_25"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04368-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,16]],"date-time":"2024-03-16T06:51:54Z","timestamp":1710571914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04368-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642043673","9783642043680"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04368-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}