| 2026 | Checking Regular Expressions in Cvc5 Proofs. | Ofec Israel, Yoni Zohar, Andrew Reynolds, S. Hitarth, Bruno Dutertre, Clark W. Barrett, Cesare Tinelli |
| 2026 | Free Set Theory - Cut Elimination and Consistency. | Andrzej Indrzejczak |
| 2026 | Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits. | Clemens Hofstadler, Daniela Kaufmann, Chen Chen |
| 2026 | An Applicative Multiset Path Order. | Nao Hirokawa, Teppei Saito, Teppei Tanaka, Wataru Yachi |
| 2026 | The ARI Infrastructure for Automated Confluence Analysis. | Nao Hirokawa, Aart Middeldorp, Teppei Saito, Ren Thiemann |
| 2026 | A Deductive Refinement Calculus for Differential-Algebraic Programs. | Jonathan Hellwig, Long Qian, Andr Platzer |
| 2026 | Completeness of Synthesis Under Realizability Assumptions Using Superposition. | Mrton Hajd, Petra Hozzov, Laura Kovcs, Eva Maria Wagner |
| 2026 | Uniform Interpolation with Constructive Diamond. | Iris van der Giessen, Ian Shillito |
| 2026 | Hardware Model Checking Certification with Certifaiger and Cerbtora. | Nils Froleyks, Emily Yu |
| 2026 | Accelerating Loops with Arrays. | Florian Frohn, Jrgen Giesl |
| 2026 | Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM. | Hugo Fre, Ian Shillito |
| 2026 | Automatically Translating Proof Systems for SMT Solvers to the λ Π-Calculus. | Ciarn Dunne, Guillaume Burel |
| 2026 | Towards Fast Automatic Verification of Textbook Proof Steps. | Adam Dingle |
| 2026 | Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT. | Emanuele Civini, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani |
| 2026 | Verification of Configurable SRA Systems. | Alessandro Cimatti, Alberto Griggio, Christian Lidstrm, Gianluca Redondi, Dylan Trenti |
| 2026 | Automating Proof Search when Equality is a Logical Connective. | Kaustuv Chaudhuri, Arunava Gantait, Dale Miller |
| 2026 | Towards Term-Based Verification of Diagrammatic Equivalence. | Julie Cailler, No Delorme, Simon Perdrix, Sophie Tourret |
| 2026 | A Two-Watched Literal Scheme for First-Order Logic. | Yasmine Briefs, Martin Bromberger, Tobias Gehl, Lorenz Leutgeb, Simon Schwarz, Christoph Weidenbach |
| 2026 | A Superposition Calculus for Separation Logic. | Tanguy Bozec, Nicolas Peltier |
| 2026 | Learning Computation Tree Logic with Neural Networks. | Benjamin Bordais, Daniel Neider, Mustafa Yaliner |
| 2026 | Growing HOLMS: A Verified Automated Prover for Grzegorczyk Logic in HOL Light. | Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi |
| 2026 | Twitch: Learning Abstractions for Equational Theorem Proving. | Guy Axelrod, Moa Johansson, Nicholas Smallbone |
| 2026 | Program Synthesis for Non-linear Real Arithmetic: Going Beyond Realizability. | S. Akshay, Supratik Chakraborty, R. Govind, Aniruddha R. Joshi |
| 2026 | Proof Nets for PiL. | Matteo Acclavio, Giulia Manara |
| 2024 | On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus. | Uwe Waldmann |