Complexity verification using guided theorem enumeration
Akhilesh Srikanth, Burak Sahin, William R. Harris · 2016
Determining if a given program satisfies a given bound on the amount of resources that it may use is a fundamental problem with critical practical applications. Conventional automatic verifiers for safety properties cannot be applied to address this problem directly because such verifiers target properties expressed in decidable theories; however, many practical bounds are expressed in nonlinear theories, which are undecidable.