{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:10:32Z","timestamp":1771024232905,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642279393","type":"print"},{"value":"9783642279409","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-27940-9_24","type":"book-chapter","created":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T02:29:29Z","timestamp":1326940169000},"page":"363-378","source":"Crossref","is-referenced-by-count":27,"title":["versat: A Verified Modern SAT Solver"],"prefix":"10.1007","author":[{"given":"Duckki","family":"Oe","sequence":"first","affiliation":[]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[]},{"given":"Corey","family":"Oliver","sequence":"additional","affiliation":[]},{"given":"Kevin","family":"Clancy","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Altenkirch, T.: Integrated verification in Type Theory. Lecture notes for a course at ESSLLI 1996, Prague (1996); Available from the author\u2019s website"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Armand, M., Gr\u00e9goire, B., Spiwack, A., Th\u00e9ry, L.: Extending Coq with Imperative Features and Its Application to SAT Verification, pp. 83\u201398 (2010)","DOI":"10.1007\/978-3-642-14052-5_8"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T. Bouton","year":"2009","unstructured":"Bouton, T., de Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: veriT: An Open, Trustable and Efficient SMT-Solver. In: Schmidt, R.A. (ed.) CADE-22 2009. LNCS, vol.\u00a05663, pp. 151\u2013156. Springer, Heidelberg (2009)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14186-7_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"R. Brummayer","year":"2010","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated Testing and Debugging of SAT and QBF Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 44\u201357. Springer, Heidelberg (2010)"},{"issue":"1","key":"24_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Conchon, S., Filli\u00e2tre, J.-C.: A persistent union-find data structure. In: Proceedings of the 2007 Workshop on Workshop on ML, pp. 37\u201346. ACM (2007)","DOI":"10.1145\/1292535.1292541"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-14808-8_18","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"A. Darbari","year":"2010","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking. In: Cavalcanti, A., D\u00e9harbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol.\u00a06255, pp. 260\u2013274. Springer, Heidelberg (2010)"},{"key":"24_CR8","unstructured":"de Moura, L., Bj\u00f8rner, N.: Proofs and Refutations, and Z3. In: Konev, B., Schmidt, R., Schulz, S. (eds.) 7th International Workshop on the Implementation of Logics, IWIL (2008)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Cimatti, A., Jones, R. (eds.) Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design, Portland, Oregon, pp. 109\u2013117. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Matthews, J., Anderson, T. (eds.) Proc. 22nd ACM Symposium on Operating Systems Principles (SOSP), pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"24_CR11","first-page":"271","volume-title":"Proceedings of the 7th International Conference on Information Processing in Sensor Networks, IPSN 2008","author":"N. Kothari","year":"2008","unstructured":"Kothari, N., Millstein, T., Govindan, R.: Deriving state machines from tinyos programs using symbolic execution. In: Proceedings of the 7th International Conference on Information Processing in Sensor Networks, IPSN 2008, pp. 271\u2013282. IEEE Computer Society, Washington, DC (2008)"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Morrisett, G., Peyton Jones, S. (eds.) 33rd ACM Symposium on Principles of Programming Languages, pp. 42\u201354. ACM Press (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"24_CR13","unstructured":"Lescuyer, S., Conchon, S.: A Reflexive Formalization of a SAT Solver in Coq. In: Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs (2008)"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F. Mari\u0107","year":"2010","unstructured":"Mari\u0107, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theor. Comput. Sci.\u00a0411, 4333\u20134356 (2010)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"24_CR15","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2005.12.005","volume":"144","author":"S. McLaughlin","year":"2006","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. Electr. Notes Theor. Comput. Sci.\u00a0144(2), 43\u201351 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-540-78800-3_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Moskal","year":"2008","unstructured":"Moskal, M.: Rocket-Fast Proof Checking for SMT Solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 486\u2013500. Springer, Heidelberg (2008)"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Oe, D., Reynolds, A., Stump, A.: Fast and Flexible Proof Checking for SMT. In: Dutertre, B., Strichman, O. (eds.) Workshop on Satisfiability Modulo Theories, SMT (2009)","DOI":"10.1145\/1670412.1670414"},{"key":"24_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2011.03.002","volume":"269","author":"N. Shankar","year":"2011","unstructured":"Shankar, N., Vaucher, M.: The mechanical verification of a dpll-based satisfiability solver. Electr. Notes Theor. Comput. Sci.\u00a0269, 3\u201317 (2011)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Stump, A., Austin, E.: Resource Typing in Guru. In: Filli\u00e2tre, J.-C., Flanagan, C. (eds.) Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, pp. 27\u201338. ACM (2010)","DOI":"10.1145\/1707790.1707796"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Stump, A., Deters, M., Petcher, A., Schiller, T., Simpson, T.: Verified Programming in Guru. In: Altenkirch, T., Millstein, T. (eds.) Programming Languges meets Program Verification, PLPV (2009)","DOI":"10.1145\/1481848.1481856"},{"issue":"2-3","key":"24_CR21","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.scico.2007.07.008","volume":"70","author":"F. Xian","year":"2008","unstructured":"Xian, F., Srisa-an, W., Jiang, H.: Garbage collection: Java application servers\u2019 Achilles heel. Science of Computer Programming\u00a070(2-3), 89\u2013110 (2008)","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27940-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,24]],"date-time":"2019-04-24T22:42:16Z","timestamp":1556145736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27940-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642279393","9783642279409"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27940-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}