Anders Schlichtkrull

I am an associate professor at Aalborg University Copenhagen (AAU CPH). I am part of the Distributed, Embedded and Intelligent Systems (DEIS) unit of the Department of Computer Science. Prevously I was assistant professor (tenure track) in the same group.

Before I was a postdoc at the Technical University of Denmark (DTU). There, I was a member of the Formal methods section of the Department of Applied Mathematics and Computer Science (DTU Compute).

I hold a PhD degree from the Department of Applied Mathematics and Computer Science (DTU Compute) where I was a PhD student in the Algorithms, Logic and Graphs (Algolog) section with main supervisor Jørgen Villadsen (DTU Compute), and co-supervisors Jasmin Blanchette (VU Amsterdam) and Thomas Bolander (DTU Compute). During my PhD studies I did a 4 month external research stay in the Automation of Logic Research Group (RG1) of the Max Planck Institute for Informatics (MPI-INF) at the Saarland Informatics Campus.

I hold a BSc degree in Software Technology from DTU and an MSc degree in Computer Science and Engineering in DTU's honors program. During my MSc study I did an exchange semester at the Technical University of Munich (TUM).

I work on formalizing logics in proof assistants. For more information, see a popular scientific abstract and an extended abstract presented at SCAI 2015. I also work on formal methods for trust and security. For more information, see the CyberSec4Europe website, and the LIGHTest website.

Awards

• DTU's Young Researcher Award 2019.
• Woody Bledsoe Award at IJCAR 2018.
• Springer Travel Award at ITP 2016.

Nominations

• Nominated for the Teacher of the Year Award 2023/2024 for Computer Science at AAU.
• Nominated for the Teacher of the Year Award 2022/2023 for Computer Science at AAU.

Publications

• Isabelle-verified correctness of Datalog programs for program analysis
  Anders Schlichtkrull, René Rydhof Hansen and Flemming Nielson.
  The 39th ACM/SIGAPP Symposium On Applied Computing (SAC2024) poster paper. 2024.
  Publisher website Preprint (PDF) Theory source
• Soundness of the Q0 proof system for higher-order logic
  Anders Schlichtkrull.
  Archive of Formal Proofs (AFP), Formal proof development. 2023.
  Website PDF Theory source
• Pushdown Systems
  Anders Schlichtkrull, Morten Konggaard Schou, Jiří Srba and Dmitriy Traytel.
  Archive of Formal Proofs (AFP), Formal proof development. 2023.
  Website PDF Theory source
• Labeled Transition Systems
  Anders Schlichtkrull, Morten Konggaard Schou, Jiří Srba and Dmitriy Traytel.
  Archive of Formal Proofs (AFP), Formal proof development. 2023.
  Website PDF Theory source
• An Experience with and Reflections on Live Coding with Active Learning
  Anders Schlichtkrull.
  International Computer Programming Education Conference (ICPEC). 2023.
  Publisher website PDF
• Verified Verifying: SMT-LIB for Strings in Isabelle
  Kevin Lotz, Mitja Kulczynski, Dirk Nowotka, Danny Bøgsted Poulsen and Anders Schlichtkrull.
  International Conference on Implementation and Application of Automata (CIAA 2023). 2023.
  Publisher website
• A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL
  Asta Halkjær From, Anders Schlichtkrull and Jørgen Villadsen.
  Journal of Logic and Computation. 2023.
  Publisher website
• Differential Testing of Pushdown Reachability with a Formally Verified Oracle
  Anders Schlichtkrull, Morten Konggaard Schou, Jiří Srba and Dmitriy Traytel.
  22nd Conference on Formal Methods in Computer-Aided Design (FMCAD'22). 2022.
  Publisher website Postprint (PDF)
• Interactive Theorem Proving for Logic and Information
  Jørgen Villadsen, Asta Halkjær From, Alexander Birch Jensen and Anders Schlichtkrull.
  Natural Language Processing in Artificial Intelligence (NLPinAI 2021). 2022.
  Publisher website Postprint (PDF)
• A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL
  Asta Halkjær From, Anders Schlichtkrull and Jørgen Villadsen.
  Italian Conference On Computational Logic (CILC 2021). 2021.
  Publisher website PDF
• Adapting the TPL Trust Policy Language for a Self-Sovereign Identity World
  Lukas Alber, Stefan More, Sebastian Mödersheim and Anders Schlichtkrull.
  Open Identity Summit 2021 (OID 2021). 2021.
  Publisher website PDF
• Performing Security Proofs of Stateful Protocols
  Andreas Viktor Hess, Sebastian Mödersheim, Achim D. Brucker and Anders Schlichtkrull.
  34th IEEE Computer Security Foundations Symposium (CSF). 2021.
  Publisher website PDF
• Are We Preparing Students to Build Security In?
  A Survey of European Cybersecurity in Higher Education Programs
  Nicola Dragoni, Alberto Lluch Lafuente, Fabio Massacci and Anders Schlichtkrull.
  IEEE Security & Privacy. 2021.
  Publisher website PDF Data and errata
• Automated Stateful Protocol Verification
  Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull.
  Archive of Formal Proofs (AFP), Formal proof development. 2020.
  Website PDF Theory source
• Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
  Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann.
  Journal of Automated Reasoning (JAR). 2020.
  Publisher website Web version Postprint (PDF)
• Teaching a Formalized Logical Calculus
  Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen.
  Proceedings 8th International Workshop on Theorem proving components for Educational software (ThEdu'19). 2020.
  Publisher website PDF
• Accountable Trust Decisions: A Semantic Approach
  Anders Schlichtkrull and Sebastian Mödersheim.
  Open Identity Summit 2020 (OID 2020). 2020.
  Publisher website PDF
• New Formalized Results on the Meta-Theory of a Paraconsistent Logic
  Anders Schlichtkrull.
  Post-proceedings of the 24th International Conference on Types for Proofs and Programs (TYPES 2019). 2019.
  Publisher website PDF
• TPL: A Trust Policy Language
  Sebastian Mödersheim, Anders Schlichtkrull, Georg Wagner, Stefan More and Lukas Alber.
  Trust Management (IFIPTM 2019). 2019.
  Publisher website Postprint (PDF)
• A Verified Prover Based on Ordered Resolution
  Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel.
  8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019). 2019.
  Publisher website PDF
• Students' Proof Assistant (SPA)
  Anders Schlichtkrull, Jørgen Villadsen, and Andreas Halkjær From.
  Proceedings 7th International Workshop on Theorem proving components for Educational software (ThEdu'18). 2019.
  Publisher website PDF
• Natural Deduction Assistant (NaDeA)
  Jørgen Villadsen, Andreas Halkjær From, and Anders Schlichtkrull.
  Proceedings 7th International Workshop on Theorem proving components for Educational software (ThEdu'18). 2019.
  Publisher website PDF
• A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
  Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel.
  Archive of Formal Proofs (AFP), Formal proof development. 2018.
  Website PDF Theory source
• Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
  Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann.
  Archive of Formal Proofs (AFP), Formal proof development. 2018.
  Website PDF Theory source
• Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
  Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann.
  9th International Joint Conference on Automated Reasoning (IJCAR 2018). 2018.
  Publisher website Postprint (PDF)
• A Verified Simple Prover for First-Order Logic
  Jørgen Villadsen, Anders Schlichtkrull, and Andreas Halkjær From.
  6th Workshop on the Practical Aspects of Automated Reasoning (PAAR 2018). 2018.
  Publisher website PDF
• Formalization of First-Order Syntactic Unification
  Kasper Fabæch Brandt, Anders Schlichtkrull, and Jørgen Villadsen.
  32nd International Workshop on Unification (UNIF 2018). 2018.
  Proceedings (PDF) PDF
• Drawing Trees
  Andreas Halkjær From, Anders Schlichtkrull, and Jørgen Villadsen.
  Isabelle Workshop 2018. 2018.
  PDF
• Substitutionless First-Order Logic: A Formal Soundness Proof
  Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull, and Jørgen Villadsen.
  Isabelle Workshop 2018. 2018.
  PDF
• Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL
  Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull, and Jørgen Villadsen.
  AI Communications. 2018.
  Publisher website Postprint (PDF)
• Formalization of the Resolution Calculus for First-Order Logic
  Anders Schlichtkrull.
  Journal of Automated Reasoning (JAR). Special Issue: Milestones in Interactive Theorem Proving. 2018.
  Publisher website Web version Postprint (PDF)
• Natural Deduction and the Isabelle Proof Assistant
  Jørgen Villadsen, Andreas Halkjær From, and Anders Schlichtkrull.
  Post-proceedings 6th International Workshop on Theorem proving components for Educational software (ThEdu'17). 2018.
  Publisher website PDF
• First-Order Logic According to Harrison
  Alexander Birch Jensen, Anders Schlichtkrull, and Jørgen Villadsen.
  Archive of Formal Proofs (AFP), Formal proof development. 2017.
  Website PDF Theory source
• Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant
  Jørgen Villadsen and Anders Schlichtkrull.
  Transactions on Large-Scale Data-and Knowledge-Centered Systems XXXIV (TLDKS). 2017.
  Publisher website Postprint (PDF)
• NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
  Jørgen Villadsen, Alexander Birch Jensen, and Anders Schlichtkrull.
  IfCoLog Journal of Logics and their Applications (FLAP). 2017.
  Publisher website PDF
• Paraconsistency
  Anders Schlichtkrull and Jørgen Villadsen.
  Archive of Formal Proofs (AFP), Formal proof development. 2016.
  Website PDF Theory source
• The Resolution Calculus for First-Order Logic
  Anders Schlichtkrull.
  Archive of Formal Proofs (AFP), Formal proof development. 2016.
  Website PDF Theory source
• Formalization of the Resolution Calculus for First-Order Logic
  Anders Schlichtkrull.
  7th International Conference on Interactive Theorem Proving (ITP 2016). 2016.
  Publisher website Postprint (PDF)
• Verification of an LCF-Style First-Order Prover with Equality
  Alexander Birch Jensen, Anders Schlichtkrull, and Jørgen Villadsen.
  Isabelle Workshop 2016. 2016.
  PDF
• Code Generation for a Simple First-Order Prover
  Jørgen Villadsen, Anders Schlichtkrull, and Andreas Halkjær From.
  Isabelle Workshop 2016. 2016
  PDF
• Formalization of Algorithms and Logical Inference Systems in Proof Assistants.
  Anders Schlichtkrull.
  13th Scandinavian Conference on Artificial Intelligence (SCAI 2015) 2015.
  Publisher website Postprint (PDF)
• Nature-Inspired and Energy Efficient Route Planning
  Anders Schlichtkrull, Jesper Bo Sembech Christensen, Thomas Feld, and Troels Buus Hansen.
  Green Challenge 2015. 2015.
  PDF
• NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
  Jørgen Villadsen, Alexander Birch Jensen, and Anders Schlichtkrull.
  4th International Conference on Tools for Teaching Logic (TTL 2015). 2015.
  PDF

Book chapter

• Formalization of Many-Valued Logics
  Jørgen Villadsen and Anders Schlichtkrull.
  Partiality and Underspecification in Information, Languages, and Knowledge
  Publisher website

Abstract

• Formalization of a Paraconsistent Infinite-Valued Logic
  Anders Schlichtkrull.
  Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018)
  Website

Poster

• Meta-Logical Reasoning in Higher-Order Logic
  Jørgen Villadsen, Anders Schlichtkrull, and Andreas Viktor Hess.
  Poster at 29th International Symposium Logica (LOGICA 2015)
  PDF

Technical Reports and Deliverables

• CyberSec4Europe D9.7: Summer Schools 1
  Alberto Lluch Lafuente and Anders Schlichtkrull. CyberSec4Europe 2020
  PDF
• CyberSec4Europe D6.2: Education and Training Review
  Nicola Dragoni, Alberto Lluch Lafuente, Anders Schlichtkrull and Luxi Zhao. CyberSec4Europe 2020
  PDF
• LIGHTest D2.6: Formal Description and Analysis of Concepts (III)
  Sebastian Mödersheim, Anders Schlichtkrull and Andreas Viktor Hess. LIGHTest 2019
  PDF
• The LIGHTest Foundation
  Sebastian Alexander Mödersheim and Anders Schlichtkrull. DTU 2018
  PDF Updated version (with author Andreas Viktor Hess) (PDF)

Theses

• Formalization of Logic in the Isabelle Proof Assistant
  Anders Schlichtkrull.
  PhD thesis, DTU Compute, Technical University of Denmark 2018
  PDF
• Formalization of the Resolution Calculus in Isabelle
  Anders Schlichtkrull.
  MSc thesis, DTU Compute, Technical University of Denmark 2015
  PDF
• Compiling Dynamic Languages
  Anders Schlichtkrull and Rasmus T. Tjalk-Bøggild.
  BSc thesis, DTU Compute, Technical University of Denmark 2013
  PDF

Software

• SML version of John Harrison's "Handbook of Practical Logic and Automated Reasoning" (Chapter 6)
  with Jørgen Villadsen.
  Website Source
• RPx
  with Jasmin Christian Blanchette and Dmitriy Traytel. Incorporates work from Metis, Isabelle, AFP and IsaFoR.
  Paper Website Source
• LIGHTest
  with the rest of the LIGHTest team.
  Website Source
• NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
  with Jørgen Villadsen, Andreas Halkjær From and Alexander Birch Jensen.
  Website Source
• CuTest: C Unit Testing Framework — AAU version
  bugfix of CuTest 1.5 made by Asim Jalis with contributions from Tobias Lippert, Eli Bendersky and Andrew Brown.
  Website Source
• IsaFoL: Isabelle Formalization of Logic
  with the other IsaFol authors.
  Website Source