An Isabelle/HOL formalization of AProVE’s termination method for LLVM IR

Max Haslbeck, Rene Thiemann
10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021),   pp. 238 – 249, 2021.

abstract   BibTeX   PDF   doi:10.1145/3437992.3439935