| 2025 | LOPSTR | Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms. | Kanta Takahata, Jonas Schpf, Naoki Nishida, Takahito Aoto |
| 2025 | PPDP | Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations. | Kanta Takahata, Jonas Schpf, Naoki Nishida, Takahito Aoto |
| 2025 | TACAS | Automated Analysis of Logically Constrained Rewrite Systems using crest. | Jonas Schpf, Aart Middeldorp |
| 2024 | FSCD | Equational Theories and Validity for Logically Constrained Term Rewriting. | Takahito Aoto, Naoki Nishida, Jonas Schpf |
| 2024 | IJCAR | Confluence of Logically Constrained Rewrite Systems Revisited. | Jonas Schpf, Fabian Mitterwallner, Aart Middeldorp |
| 2023 | CADE | Confluence Criteria for Logically Constrained Rewrite Systems. | Jonas Schpf, Aart Middeldorp |
| 2020 | FSCD | Certifying the Weighted Path Order (Invited Talk). | Ren Thiemann, Jonas Schpf, Christian Sternagel, Akihisa Yamada |
| 2018 | ITP | A Formally Verified Solver for Homogeneous Linear Diophantine Equations. | Florian Mener, Julian Parsert, Jonas Schpf, Christian Sternagel |