| SPASS Version 3.5 C Weidenbach, D Dimova, A Fietzke, R Kumar, M Suda, P Wischnewski Automated Deduction–CADE-22: 22nd International Conference on Automated …, 2009 | 436 | 2009 |
| Computing small clause normal forms A Nonnengart, C Weidenbach Handbook of automated reasoning, 335-367, 2001 | 315 | 2001 |
| SPASS: Combining superposition, sorts and splitting C Weidenbach Handbook of automated reasoning 2, 1965-2013, 1999 | 306 | 1999 |
| Towards an automatic analysis of security protocols in first-order logic C Weidenbach International Conference on Automated Deduction, 314-328, 1999 | 254 | 1999 |
| Spass Version 2.0 C Weidenbach, U Brahm, T Hillenbrand, E Keen, C Theobald, D Topić Automated Deduction—CADE-18: 18th International Conference on Automated …, 2002 | 220* | 2002 |
| System description: Spass version 1.0. 0 C Weidenbach, B Afshordel, U Brahm, C Cohrs, T Engel, E Keen, ... CADE, 378-382, 1999 | 209* | 1999 |
| Spass & flotter version 0.42 C Weidenbach, B Gaede, G Rock Automated Deduction—Cade-13: 13th International Conference on Automated …, 1996 | 169 | 1996 |
| On generating small clause normal forms A Nonnengart, G Rock, C Weidenbach Automated Deduction—CADE-15: 15th International Conference on Automated …, 1998 | 92 | 1998 |
| A verified SAT solver framework with learn, forget, restart, and incrementality JC Blanchette, M Fleury, P Lammich, C Weidenbach Journal of automated reasoning 61, 333-365, 2018 | 91 | 2018 |
| SPASS-Version 0.49 C Weidenbach Journal of Automated Reasoning 18, 247-252, 1997 | 80 | 1997 |
| Superposition modulo linear arithmetic SUP (LA) E Althaus, E Kruglov, C Weidenbach International Symposium on Frontiers of Combining Systems, 84-99, 2009 | 76 | 2009 |
| Saturation-based decision procedures for extensions of the guarded fragment Y Kazakov Universität des Saarlandes Saarbrücken, 2006 | 67 | 2006 |
| Towards Verification of the Pastry Protocol Using TLA + T Lu, S Merz, C Weidenbach International Conference on Formal Methods for Open Object-Based Distributed …, 2011 | 59 | 2011 |
| More SPASS with Isabelle: Superposition with hard sorts and configurable simplification JC Blanchette, A Popescu, D Wand, C Weidenbach Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 51 | 2012 |
| Soft typing for ordered resolution H Ganzinger, C Meyer, C Weidenbach Automated Deduction—CADE-14: 14th International Conference on Automated …, 1997 | 51 | 1997 |
| Unification in extensions of shallow equational theories F Jacquemard, C Meyer, C Weidenbach Rewriting Techniques and Applications: 9th International Conference, RTA-98 …, 1998 | 45 | 1998 |
| First-order tableaux with sorts C Weidenbach Logic Journal of the IGPL 3 (6), 887-906, 1995 | 44 | 1995 |
| A PLTL-prover based on labelled superposition with partial model guidance M Suda, C Weidenbach Automated Reasoning: 6th International Joint Conference, IJCAR 2012 …, 2012 | 41 | 2012 |
| MSPASS: Subsumption Testing with SPASS. U Hustadt, RA Schmidt, C Weidenbach Description Logics, 1999 | 41 | 1999 |
| Unification in sort theories and its applications C Weidenbach Annals of Mathematics and Artificial Intelligence 18, 261-293, 1996 | 37 | 1996 |
