Mining the Archive of Formal Proofs. - Jasmin Christian Blanchette; Max W. Haslbeck; Daniel Matichuk; Tobias Nipkow (CICM, 2015)

Verified iptables firewall analysis. - Cornelius Diekmann; Julius Michaelis; Max W. Haslbeck; Georg Carle (Networking, 2016)

Simple Firewall. - Cornelius Diekmann; Julius Michaelis; Max W. Haslbeck (Arch. Formal Proofs, 2016)

Algorithms for Reduced Ordered Binary Decision Diagrams. - Julius Michaelis; Max W. Haslbeck; Peter Lammich; Lars Hupel (Arch. Formal Proofs, 2016)

A Verified Efficient Implementation of the LLL Basis Reduction Algorithm. - Ralph Bottesch; Max W. Haslbeck; René Thiemann (LPAR, 2018)

Treaps. - Max W. Haslbeck; Manuel Eberl; Tobias Nipkow (Arch. Formal Proofs, 2018)

Verified iptables Firewall Analysis and Verification. - Cornelius Diekmann; Lars Hupel; Julius Michaelis; Max W. Haslbeck; Georg Carle (J. Autom. Reason., 2018)

Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL. - Ralph Bottesch; Max W. Haslbeck; René Thiemann (FroCos, 2019)

Farkas' Lemma and Motzkin's Transposition Theorem. - Ralph Bottesch; Max W. Haslbeck; René Thiemann (Arch. Formal Proofs, 2019)

Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL. - Ralph Bottesch; Max W. Haslbeck; Alban Reynaud; René Thiemann (NFM, 2020)

Skip Lists. - Max W. Haslbeck; Manuel Eberl (Arch. Formal Proofs, 2020)

Verified Analysis of Random Binary Tree Structures. - Manuel Eberl; Max W. Haslbeck; Tobias Nipkow (J. Autom. Reason., 2020)

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. - René Thiemann; Ralph Bottesch; Jose Divasón; Max W. Haslbeck; Sebastiaan J. C. Joosten; Akihisa Yamada 002 (J. Autom. Reason., 2020)

An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. - Max W. Haslbeck; René Thiemann (CPP, 2021)