| 2025 | Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification. | Yi Zhou, Amar Shah, Zhengyao Lin, Marijn Heule, Bryan Parno |
| 2025 | Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT. | Yizheng Zhao, Junyi Zhang, Renate A. Schmidt |
| 2025 | Being Polite Is Not Enough (and Other Limits of Theory Combination). | Guilherme Vicentin de Toledo, Benjamin Przybocki, Yoni Zohar |
| 2025 | Efficient Neural Clause-Selection Reinforcement. | Martin Suda |
| 2025 | Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm. | Lukas Stevens, Rebecca Ghidini |
| 2025 | On Symbol Elimination and Uniform Interpolation in Theory Extensions. | Viorica Sofronie-Stokkermans |
| 2025 | A Theorem Prover Based Approach for SAT-Based Model Checking Certification. | Giulia Sindoni, Paolo Pasini, Gianpiero Cabodi, Paolo E. Camurati, Alberto Griggio, Marco Palena, Marco Roveri, Stefano Tonetta |
| 2025 | Entailment vs. Verification for Partial-Assignment Satisfiability and Enumeration. | Roberto Sebastiani |
| 2025 | Lexicographic Combination of Reduction Pairs. | Teppei Saito, Nao Hirokawa |
| 2025 | Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories. | Michael Rawson, Andrei Voronkov, Johannes Schoisswohl, Anja Petkovic Komel |
| 2025 | Unfolding Boxes with Local Constraints. | Long Qian, Eric Wang, Bernardo Subercaseaux, Marijn J. H. Heule |
| 2025 | More is Less: Adding Polynomials for Faster Explanations in NLSAT. | Valentin Promies, Jasper Nalbach, Erika brahm, Paul Wagner |
| 2025 | From Modal Sequent Calculi to Modal Resolution. | Dirk Pattinson, Cludia Nalon, Sourabh Peruri |
| 2025 | Anti-pattern Templates. | Jan Otop |
| 2025 | The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting. | Johannes Niederhauser, Aart Middeldorp |
| 2025 | Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems. | Salvador Lucas |
| 2025 | Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. | Enrico Lipparini, Thomas Hader, Ahmed Irfan, Stphane Graham-Lengrand |
| 2025 | Computing Ground Congruence Classes. | Hendrik Leidinger, Christoph Weidenbach |
| 2025 | Cut Elimination for Negative Free Logics with Definite Descriptions. | Andrzej Indrzejczak |
| 2025 | What's Decidable About Arrays With Sums? | Roland Herrmann, Philipp Rmmer |
| 2025 | A Real-Analytic Approach to Differential-Algebraic Dynamic Logic. | Jonathan Hellwig, Andr Platzer |
| 2025 | Partial Redundancy in Saturation. | Mrton Hajd, Laura Kovcs, Andrei Voronkov |
| 2025 | Term Ordering Diagrams. | Mrton Hajd, Robin Coutelier, Laura Kovcs, Andrei Voronkov |
| 2025 | Interoperability of Proof Systems with SC-TPTP. | Simon Guilloud, Julie Cailler, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, Viktor Kuncak |
| 2025 | Relatively Complete and Efficient Partial Quantifier Elimination. | Estifanos Getachew, Arie Gurfinkel, Richard J. Trefler |