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

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439935 ◽

2021 ◽

Author(s):

Max W. Haslbeck ◽

René Thiemann

Download Full-text