{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T19:10:10Z","timestamp":1750360210847,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319614663"},{"type":"electronic","value":"9783319614670"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-61467-0_10","type":"book-chapter","created":{"date-parts":[[2017,6,17]],"date-time":"2017-06-17T04:33:58Z","timestamp":1497674038000},"page":"152-161","source":"Crossref","is-referenced-by-count":2,"title":["Testing a Saturation-Based Theorem Prover: Experiences and Challenges"],"prefix":"10.1007","author":[{"given":"Giles","family":"Reger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,6,18]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38916-0_3","volume-title":"Tests and Proofs","author":"C Artho","year":"2013","unstructured":"Artho, C., Biere, A., Seidl, M.: Model-based testing for verification back-ends. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 39\u201355. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38916-0_3"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, vol. 1, chap. 2, pp. 19\u201399. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_14"},{"key":"10_CR4","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). www.SMT-LIB.org"},{"key":"10_CR5","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","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. 6175, pp. 44\u201357. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14186-7_6"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-30473-6_14","volume-title":"Tests and Proofs","author":"N Creignou","year":"2012","unstructured":"Creignou, N., Egly, U., Seidl, M.: A framework for the specification of random SAT and QSAT formulas. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 163\u2013168. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-30473-6_14"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-39910-0_14","volume-title":"Verification: Theory and Practice","author":"N Dershowitz","year":"2003","unstructured":"Dershowitz, N., Jayasimha, D.N., Park, S.: Bounded fairness. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 304\u2013317. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-39910-0_14"},{"key":"10_CR8","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/j.tcs.2014.02.052","volume":"537","author":"V Diekert","year":"2014","unstructured":"Diekert, V., Leucker, M.: Topology, monitorable properties and runtime verification. Theor. Comput. Sci. 537, 29\u201341 (2014). Theoretical Aspects of Computing (ICTAC 2011)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-04694-0_4","volume-title":"Runtime Verification","author":"Y Falcone","year":"2009","unstructured":"Falcone, Y., Fernandez, J.C., Mounier, L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40\u201359. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04694-0_4"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-319-40229-1_22","volume-title":"Automated Reasoning","author":"K Hoder","year":"2016","unstructured":"Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 313\u2013329. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1_22"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction - CADE-23","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 299\u2013314. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_23"},{"issue":"1","key":"10_CR12","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Hol(y)hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_24"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_1"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: The 8th International Workshop on the Implementation of Logics, IWIL 2010. EPiC Series in Computing, vol. 2, pp. 1\u201311. EasyChair (2012)","DOI":"10.29007\/36dt"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Perrouin, G., Sen, S., Klein, J., Baudry, B., Traon, Y.l.: Automated and scalable t-wise test case generation strategies for software product lines. In: Proceedings of the 2010 Third International Conference on Software Testing, Verification and Validation, ICST 2010, pp. 459\u2013468. IEEE Computer Society (2010)","DOI":"10.1109\/ICST.2010.43"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Reger, G.: Better proof output for Vampire. In: Proceedings of the 3rd Vampire Workshop, Vampire 2016. EPiC Series in Computing, vol. 44, pp. 46\u201360. EasyChair (2017)","DOI":"10.29007\/5dmz"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M.: The uses of sat solvers in vampire. In: Proceedings of the 1st and 2nd Vampire Workshops. EPiC Series in Computing, vol. 38, pp. 63\u201369. EasyChair (2016)","DOI":"10.29007\/4w68"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: 2nd Global Conference on Artificial Intelligence, GCAI 2016. EPiC Series in Computing, vol. 41, pp. 11\u201323. EasyChair (2016)","DOI":"10.29007\/dzfz"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). ArXiv e-prints (2017)","DOI":"10.1007\/978-3-319-61467-0_10"},{"issue":"1\u20132","key":"10_CR21","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","volume":"36","author":"A Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. J. Symb. Comput. 36(1\u20132), 101\u2013115 (2003)","journal-title":"J. Symb. Comput."},{"issue":"2\u20133","key":"10_CR22","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"issue":"6","key":"10_CR23","doi-asserted-by":"crossref","first-page":"1053","DOI":"10.1142\/S0218213006003119","volume":"15","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: Semantic derivation verification: techniques and implementation. Int. J. Artif. Intell. Tools 15(6), 1053\u20131070 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"issue":"4","key":"10_CR24","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"10_CR25","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction - CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02959-2_10"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48166-4_16","volume-title":"Software Engineering","author":"A Zeller","year":"1999","unstructured":"Zeller, A.: Yesterday, my program worked. Today, it does not. Why? In: Nierstrasz, O., Lemoine, M. (eds.) ESEC\/FSE 1999. LNCS, vol. 1687, pp. 253\u2013267. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48166-4_16"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-61467-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T18:39:24Z","timestamp":1750358364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-61467-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319614663","9783319614670"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-61467-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}