{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,12]],"date-time":"2025-08-12T22:02:21Z","timestamp":1755036141204},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540330561"},{"type":"electronic","value":"9783540330578"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11691372_11","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:22:26Z","timestamp":1143555746000},"page":"167-181","source":"Crossref","is-referenced-by-count":46,"title":["Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Fontaine","sequence":"first","affiliation":[]},{"given":"Jean-Yves","family":"Marion","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[]},{"given":"Leonor Prensa","family":"Nieto","sequence":"additional","affiliation":[]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/B978-044450813-3\/50007-2","volume-title":"Handbook of Automated Reasoning, ch. 5","author":"M. Baaz","year":"2001","unstructured":"Baaz, M., Egly, U., Leitsch, A.: Normal form transformations. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 5, vol.\u00a0I, pp. 273\u2013333. Elsevier Science B.V, Amsterdam (2001)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Barsotti, D., Prensa-Nieto, L., Tiu, A.: Verification of clock synchronization algorithms: Experiments on a combination of deductive tools. In: Proc. of the Fifth Workshop on Automated Verification of Critical Systems (AVOCS), ENTCS (to appear) (2005)","DOI":"10.1016\/j.entcs.2005.10.005"},{"issue":"3-4","key":"11_CR4","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M. Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. J. Autom. Reasoning\u00a029(3-4), 253\u2013275 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"11_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/11532231_23","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: The MathSAT 3 System. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 315\u2013321. Springer, Heidelberg (2005)"},{"issue":"7","key":"11_CR6","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Comm. of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Comm. of the ACM"},{"key":"11_CR7","first-page":"220","volume-title":"Software Engineering and Formal Methods (SEFM)","author":"D. D\u00e9harbe","year":"2003","unstructured":"D\u00e9harbe, D., Ranise, S.: Light-weight theorem proving for debugging and verifying units of code. In: Software Engineering and Formal Methods (SEFM), pp. 220\u2013228. IEEE Comp. Soc, Los Alamitos (2003)"},{"issue":"4","key":"11_CR8","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P.J. Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. Journal of the ACM\u00a027(4), 758\u2013771 (1980)","journal-title":"Journal of the ACM"},{"key":"11_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":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"key":"11_CR11","unstructured":"Fontaine, P.: Techniques for verification of concurrent systems with invariants. PhD thesis, Institut Montefiore, Universit\u00e9 de Li\u00e9ge, Belgium (September 2004)"},{"key":"11_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/3-540-36078-6_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Fontaine","year":"2002","unstructured":"Fontaine, P., Gribomont, E.P.: Using BDDs with combinations of theories. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 190\u2013201. Springer, Heidelberg (2002)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013322. Springer, Heidelberg (1999)"},{"key":"11_CR14","unstructured":"Mahboubi, A.: Programming and certifying the CAD algorithm inside the coq system. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs, Schloss Dagstuhl, Germany. Dagstuhl Seminar Proceedings, vol.\u00a005021 (2005)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/10721959_37","volume-title":"Automated Deduction - CADE-17","author":"A. Meier","year":"2000","unstructured":"Meier, A.: TRAMP: Transformation of machine-found proofs into ND-proofs at the assertion level. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 460\u2013464. Springer, Heidelberg (2000)"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Information and Computation (to appear)","DOI":"10.1016\/j.ic.2005.05.010"},{"key":"11_CR17","first-page":"112","volume":"85","author":"D.G. Mitchell","year":"2005","unstructured":"Mitchell, D.G.: A SAT solver primer. EATCS Bulletin\u00a085, 112\u2013133 (2005)","journal-title":"EATCS Bulletin"},{"key":"11_CR18","first-page":"93","volume-title":"Logics in Computer Science (LICS 1998)","author":"G. Necula","year":"1998","unstructured":"Necula, G., Lee, P.: Efficient representation and validation of logical proofs. In: Logics in Computer Science (LICS 1998), pp. 93\u2013104. IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"11_CR19","unstructured":"Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University, Available as Technical Report CMU-CS-98-154 (October 1998)"},{"issue":"2","key":"11_CR20","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"issue":"3-4","key":"11_CR21","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1023\/A:1021975117537","volume":"29","author":"Q.H. Nguyen","year":"2002","unstructured":"Nguyen, Q.H., Kirchner, C., Kirchner, H.: External rewriting for skeptical proof assistants. J. Autom. Reason.\u00a029(3-4), 309\u2013336 (2002)","journal-title":"J. Autom. Reason."},{"key":"11_CR22","unstructured":"Nieuwenhuis, R., Oliveras, A.: Union-find and congruence closure algorithms that produce proofs. In: Tinelli, C., Ranise, S. (eds.) PDPAR (2004)"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"11_CR24","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.1 (March 2005)"},{"key":"11_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-45620-1_12","volume-title":"Automated Deduction - CADE-18","author":"J.H. Siekmann","year":"2002","unstructured":"Siekmann, J.H., et al.: Proof development with \u03a9MEGA. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 144\u2013149. Springer, Heidelberg (2002)"},{"key":"11_CR26","unstructured":"Tiu, A.: Formalization of a generalized protocol for clock synchronization in Isabelle\/HOL. Archive of Formal Proofs (2005), http:\/\/afp.sourceforge.net"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, vol.\u00a0II, pp. 115\u2013125 (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"11_CR28","unstructured":"Weber, T.: Using a SAT solver as a fast decision procedure for propositional logic in an LCF-style theorem prover. In: Hurd, J., Smith, E., Darbari, A. (eds.) TPHOLs 2005. Emerging Trends, pp. 180\u2013189. Oxford Univ. Comp. Lab., Prog. Res. Group (2005)"},{"key":"11_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/3-540-45620-1_26","volume-title":"Automated Deduction - CADE-18","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The quest for efficient Boolean satisfiability solvers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 295\u2013313. Springer, Heidelberg (2002)"},{"key":"11_CR30","first-page":"10880","volume-title":"Design, Automation and Test in Europe (DATE 2003)","author":"L. Zhang","year":"2003","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker. In: Design, Automation and Test in Europe (DATE 2003), pp. 10880\u201310885. IEEE Comp. Soc., Los Alamitos (2003)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691372_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T17:19:21Z","timestamp":1555521561000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691372_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540330561","9783540330578"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/11691372_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}