| 2025 | ITP | Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness la Fitting. | Asta Halkjr From, Anders Schlichtkrull |
| 2025 | PPDP | Formalizing Weighted Pushdown Systems in Isabelle/HOL. | Anders Schlichtkrull, Morten Konggaard Schou |
| 2024 | SAC | Isabelle-verified correctness of Datalog programs for program analysis. | Anders Schlichtkrull, Ren Rydhof Hansen, Flemming Nielson |
| 2022 | FMCAD | Differential Testing of Pushdown Reachability with a Formally Verified Oracle. | Anders Schlichtkrull, Morten Konggaard Schou, Jir Srba, Dmitriy Traytel |
| 2019 | CPP | A verified prover based on ordered resolution. | Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel |
| 2018 | CADE | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. | Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann |
| 2018 | CADE | A Verified Simple Prover for First-Order Logic. | Jrgen Villadsen, Anders Schlichtkrull, Asta Halkjr From |
| 2016 | ITP | Formalization of the Resolution Calculus for First-Order Logic. | Anders Schlichtkrull |